Theorem lfnnth ≪ | index | src | ≫ 

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