Theorem lfnnth ≪ | index | src | ≫ 

theorem lfnnth {i: nat} (l: nat): $ lfn (\ i, nth i l - 1) (len l) = l $;
StepHypRefExpression
1 eqidd 
_1 = l -> i = i
2 id 
_1 = l -> _1 = l
3 1, 2 ntheqd 
_1 = l -> nth i _1 = nth i l
4 eqidd 
_1 = l -> 1 = 1
5 3, 4 subeqd 
_1 = l -> nth i _1 - 1 = nth i l - 1
6 5 lameqd 
_1 = l -> \ i, nth i _1 - 1 == \ i, nth i l - 1
7 2 leneqd 
_1 = l -> len _1 = len l
8 6, 7 lfneqd 
_1 = l -> lfn (\ i, nth i _1 - 1) (len _1) = lfn (\ i, nth i l - 1) (len l)
9 8, 2 eqeqd 
_1 = l -> (lfn (\ i, nth i _1 - 1) (len _1) = _1 <-> lfn (\ i, nth i l - 1) (len l) = l)
10 eqidd 
_1 = 0 -> i = i
11 id 
_1 = 0 -> _1 = 0
12 10, 11 ntheqd 
_1 = 0 -> nth i _1 = nth i 0
13 eqidd 
_1 = 0 -> 1 = 1
14 12, 13 subeqd 
_1 = 0 -> nth i _1 - 1 = nth i 0 - 1
15 14 lameqd 
_1 = 0 -> \ i, nth i _1 - 1 == \ i, nth i 0 - 1
16 11 leneqd 
_1 = 0 -> len _1 = len 0
17 15, 16 lfneqd 
_1 = 0 -> lfn (\ i, nth i _1 - 1) (len _1) = lfn (\ i, nth i 0 - 1) (len 0)
18 17, 11 eqeqd 
_1 = 0 -> (lfn (\ i, nth i _1 - 1) (len _1) = _1 <-> lfn (\ i, nth i 0 - 1) (len 0) = 0)
19 eqidd 
_1 = a2 -> i = i
20 id 
_1 = a2 -> _1 = a2
21 19, 20 ntheqd 
_1 = a2 -> nth i _1 = nth i a2
22 eqidd 
_1 = a2 -> 1 = 1
23 21, 22 subeqd 
_1 = a2 -> nth i _1 - 1 = nth i a2 - 1
24 23 lameqd 
_1 = a2 -> \ i, nth i _1 - 1 == \ i, nth i a2 - 1
25 20 leneqd 
_1 = a2 -> len _1 = len a2
26 24, 25 lfneqd 
_1 = a2 -> lfn (\ i, nth i _1 - 1) (len _1) = lfn (\ i, nth i a2 - 1) (len a2)
27 26, 20 eqeqd 
_1 = a2 -> (lfn (\ i, nth i _1 - 1) (len _1) = _1 <-> lfn (\ i, nth i a2 - 1) (len a2) = a2)
28 eqidd 
_1 = a1 : a2 -> i = i
29 id 
_1 = a1 : a2 -> _1 = a1 : a2
30 28, 29 ntheqd 
_1 = a1 : a2 -> nth i _1 = nth i (a1 : a2)
31 eqidd 
_1 = a1 : a2 -> 1 = 1
32 30, 31 subeqd 
_1 = a1 : a2 -> nth i _1 - 1 = nth i (a1 : a2) - 1
33 32 lameqd 
_1 = a1 : a2 -> \ i, nth i _1 - 1 == \ i, nth i (a1 : a2) - 1
34 29 leneqd 
_1 = a1 : a2 -> len _1 = len (a1 : a2)
35 33, 34 lfneqd 
_1 = a1 : a2 -> lfn (\ i, nth i _1 - 1) (len _1) = lfn (\ i, nth i (a1 : a2) - 1) (len (a1 : a2))
36 35, 29 eqeqd 
_1 = a1 : a2 -> (lfn (\ i, nth i _1 - 1) (len _1) = _1 <-> lfn (\ i, nth i (a1 : a2) - 1) (len (a1 : a2)) = a1 : a2)
37 eqtr 
lfn (\ i, nth i 0 - 1) (len 0) = lfn (\ i, nth i 0 - 1) 0 -> lfn (\ i, nth i 0 - 1) 0 = 0 -> lfn (\ i, nth i 0 - 1) (len 0) = 0
38 lfneq2 
len 0 = 0 -> lfn (\ i, nth i 0 - 1) (len 0) = lfn (\ i, nth i 0 - 1) 0
39 len0 
len 0 = 0
40 38, 39 ax_mp 
lfn (\ i, nth i 0 - 1) (len 0) = lfn (\ i, nth i 0 - 1) 0
41 37, 40 ax_mp 
lfn (\ i, nth i 0 - 1) 0 = 0 -> lfn (\ i, nth i 0 - 1) (len 0) = 0
42 lfnaux0 
lfnaux (\ i, nth i 0 - 1) 0 0 = 0
43 42 conv lfn 
lfn (\ i, nth i 0 - 1) 0 = 0
44 41, 43 ax_mp 
lfn (\ i, nth i 0 - 1) (len 0) = 0
45 lfneq2 
len (a1 : a2) = suc (len a2) -> lfn (\ i, nth i (a1 : a2) - 1) (len (a1 : a2)) = lfn (\ i, nth i (a1 : a2) - 1) (suc (len a2))
46 lenS 
len (a1 : a2) = suc (len a2)
47 45, 46 ax_mp 
lfn (\ i, nth i (a1 : a2) - 1) (len (a1 : a2)) = lfn (\ i, nth i (a1 : a2) - 1) (suc (len a2))
48 lfnS 
lfn (\ i, nth i (a1 : a2) - 1) (suc (len a2)) = (\ i, nth i (a1 : a2) - 1) @ 0 : lfn (\ a3, (\ i, nth i (a1 : a2) - 1) @ suc a3) (len a2)
49 conseq 
(\ i, nth i (a1 : a2) - 1) @ 0 = a1 ->
  lfn (\ a3, (\ i, nth i (a1 : a2) - 1) @ suc a3) (len a2) = lfn (\ i, nth i a2 - 1) (len a2) ->
  (\ i, nth i (a1 : a2) - 1) @ 0 : lfn (\ a3, (\ i, nth i (a1 : a2) - 1) @ suc a3) (len a2) = a1 : lfn (\ i, nth i a2 - 1) (len a2)
50 sucsub1 
suc a1 - 1 = a1
51 nthZ 
nth 0 (a1 : a2) = suc a1
52 ntheq1 
i = 0 -> nth i (a1 : a2) = nth 0 (a1 : a2)
53 51, 52 syl6eq 
i = 0 -> nth i (a1 : a2) = suc a1
54 53 subeq1d 
i = 0 -> nth i (a1 : a2) - 1 = suc a1 - 1
55 50, 54 syl6eq 
i = 0 -> nth i (a1 : a2) - 1 = a1
56 55 applame 
(\ i, nth i (a1 : a2) - 1) @ 0 = a1
57 49, 56 ax_mp 
lfn (\ a3, (\ i, nth i (a1 : a2) - 1) @ suc a3) (len a2) = lfn (\ i, nth i a2 - 1) (len a2) ->
  (\ i, nth i (a1 : a2) - 1) @ 0 : lfn (\ a3, (\ i, nth i (a1 : a2) - 1) @ suc a3) (len a2) = a1 : lfn (\ i, nth i a2 - 1) (len a2)
58 lfneq1 
\ a3, (\ i, nth i (a1 : a2) - 1) @ suc a3 == \ i, nth i a2 - 1 -> lfn (\ a3, (\ i, nth i (a1 : a2) - 1) @ suc a3) (len a2) = lfn (\ i, nth i a2 - 1) (len a2)
59 eqstr 
\ a3, (\ i, nth i (a1 : a2) - 1) @ suc a3 == \ a3, nth a3 a2 - 1 ->
  \ a3, nth a3 a2 - 1 == \ i, nth i a2 - 1 ->
  \ a3, (\ i, nth i (a1 : a2) - 1) @ suc a3 == \ i, nth i a2 - 1
60 nthS 
nth (suc a3) (a1 : a2) = nth a3 a2
61 ntheq1 
i = suc a3 -> nth i (a1 : a2) = nth (suc a3) (a1 : a2)
62 60, 61 syl6eq 
i = suc a3 -> nth i (a1 : a2) = nth a3 a2
63 62 subeq1d 
i = suc a3 -> nth i (a1 : a2) - 1 = nth a3 a2 - 1
64 63 applame 
(\ i, nth i (a1 : a2) - 1) @ suc a3 = nth a3 a2 - 1
65 64 lameqi 
\ a3, (\ i, nth i (a1 : a2) - 1) @ suc a3 == \ a3, nth a3 a2 - 1
66 59, 65 ax_mp 
\ a3, nth a3 a2 - 1 == \ i, nth i a2 - 1 -> \ a3, (\ i, nth i (a1 : a2) - 1) @ suc a3 == \ i, nth i a2 - 1
67 ntheq1 
a3 = i -> nth a3 a2 = nth i a2
68 67 subeq1d 
a3 = i -> nth a3 a2 - 1 = nth i a2 - 1
69 68 cbvlam 
\ a3, nth a3 a2 - 1 == \ i, nth i a2 - 1
70 66, 69 ax_mp 
\ a3, (\ i, nth i (a1 : a2) - 1) @ suc a3 == \ i, nth i a2 - 1
71 58, 70 ax_mp 
lfn (\ a3, (\ i, nth i (a1 : a2) - 1) @ suc a3) (len a2) = lfn (\ i, nth i a2 - 1) (len a2)
72 57, 71 ax_mp 
(\ i, nth i (a1 : a2) - 1) @ 0 : lfn (\ a3, (\ i, nth i (a1 : a2) - 1) @ suc a3) (len a2) = a1 : lfn (\ i, nth i a2 - 1) (len a2)
73 conseq2 
lfn (\ i, nth i a2 - 1) (len a2) = a2 -> a1 : lfn (\ i, nth i a2 - 1) (len a2) = a1 : a2
74 72, 73 syl5eq 
lfn (\ i, nth i a2 - 1) (len a2) = a2 -> (\ i, nth i (a1 : a2) - 1) @ 0 : lfn (\ a3, (\ i, nth i (a1 : a2) - 1) @ suc a3) (len a2) = a1 : a2
75 48, 74 syl5eq 
lfn (\ i, nth i a2 - 1) (len a2) = a2 -> lfn (\ i, nth i (a1 : a2) - 1) (suc (len a2)) = a1 : a2
76 47, 75 syl5eq 
lfn (\ i, nth i a2 - 1) (len a2) = a2 -> lfn (\ i, nth i (a1 : a2) - 1) (len (a1 : a2)) = a1 : a2
77 9, 18, 27, 36, 44, 76 listind 
lfn (\ i, nth i l - 1) (len l) = l

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)