Theorem appendnth1 ≪ | index | src | ≫ 

theorem appendnth1 (i l1 l2: nat):
  $ i < len l1 -> nth i (l1 ++ l2) = nth i l1 $;
StepHypRefExpression
1 lteq1 
a3 = i -> (a3 < len l1 <-> i < len l1)
2 ntheq1 
a3 = i -> nth a3 (l1 ++ l2) = nth i (l1 ++ l2)
3 ntheq1 
a3 = i -> nth a3 l1 = nth i l1
4 2, 3 eqeqd 
a3 = i -> (nth a3 (l1 ++ l2) = nth a3 l1 <-> nth i (l1 ++ l2) = nth i l1)
5 1, 4 imeqd 
a3 = i -> (a3 < len l1 -> nth a3 (l1 ++ l2) = nth a3 l1 <-> i < len l1 -> nth i (l1 ++ l2) = nth i l1)
6 5 eale 
A. a3 (a3 < len l1 -> nth a3 (l1 ++ l2) = nth a3 l1) -> i < len l1 -> nth i (l1 ++ l2) = nth i l1
7 id 
_1 = l1 -> _1 = l1
8 7 leneqd 
_1 = l1 -> len _1 = len l1
9 8 lteq2d 
_1 = l1 -> (a3 < len _1 <-> a3 < len l1)
10 7 appendeq1d 
_1 = l1 -> _1 ++ l2 = l1 ++ l2
11 10 ntheq2d 
_1 = l1 -> nth a3 (_1 ++ l2) = nth a3 (l1 ++ l2)
12 7 ntheq2d 
_1 = l1 -> nth a3 _1 = nth a3 l1
13 11, 12 eqeqd 
_1 = l1 -> (nth a3 (_1 ++ l2) = nth a3 _1 <-> nth a3 (l1 ++ l2) = nth a3 l1)
14 9, 13 imeqd 
_1 = l1 -> (a3 < len _1 -> nth a3 (_1 ++ l2) = nth a3 _1 <-> a3 < len l1 -> nth a3 (l1 ++ l2) = nth a3 l1)
15 14 aleqd 
_1 = l1 -> (A. a3 (a3 < len _1 -> nth a3 (_1 ++ l2) = nth a3 _1) <-> A. a3 (a3 < len l1 -> nth a3 (l1 ++ l2) = nth a3 l1))
16 id 
_1 = 0 -> _1 = 0
17 16 leneqd 
_1 = 0 -> len _1 = len 0
18 17 lteq2d 
_1 = 0 -> (a3 < len _1 <-> a3 < len 0)
19 16 appendeq1d 
_1 = 0 -> _1 ++ l2 = 0 ++ l2
20 19 ntheq2d 
_1 = 0 -> nth a3 (_1 ++ l2) = nth a3 (0 ++ l2)
21 16 ntheq2d 
_1 = 0 -> nth a3 _1 = nth a3 0
22 20, 21 eqeqd 
_1 = 0 -> (nth a3 (_1 ++ l2) = nth a3 _1 <-> nth a3 (0 ++ l2) = nth a3 0)
23 18, 22 imeqd 
_1 = 0 -> (a3 < len _1 -> nth a3 (_1 ++ l2) = nth a3 _1 <-> a3 < len 0 -> nth a3 (0 ++ l2) = nth a3 0)
24 23 aleqd 
_1 = 0 -> (A. a3 (a3 < len _1 -> nth a3 (_1 ++ l2) = nth a3 _1) <-> A. a3 (a3 < len 0 -> nth a3 (0 ++ l2) = nth a3 0))
25 id 
_1 = a2 -> _1 = a2
26 25 leneqd 
_1 = a2 -> len _1 = len a2
27 26 lteq2d 
_1 = a2 -> (a3 < len _1 <-> a3 < len a2)
28 25 appendeq1d 
_1 = a2 -> _1 ++ l2 = a2 ++ l2
29 28 ntheq2d 
_1 = a2 -> nth a3 (_1 ++ l2) = nth a3 (a2 ++ l2)
30 25 ntheq2d 
_1 = a2 -> nth a3 _1 = nth a3 a2
31 29, 30 eqeqd 
_1 = a2 -> (nth a3 (_1 ++ l2) = nth a3 _1 <-> nth a3 (a2 ++ l2) = nth a3 a2)
32 27, 31 imeqd 
_1 = a2 -> (a3 < len _1 -> nth a3 (_1 ++ l2) = nth a3 _1 <-> a3 < len a2 -> nth a3 (a2 ++ l2) = nth a3 a2)
33 32 aleqd 
_1 = a2 -> (A. a3 (a3 < len _1 -> nth a3 (_1 ++ l2) = nth a3 _1) <-> A. a3 (a3 < len a2 -> nth a3 (a2 ++ l2) = nth a3 a2))
34 id 
_1 = a1 : a2 -> _1 = a1 : a2
35 34 leneqd 
_1 = a1 : a2 -> len _1 = len (a1 : a2)
36 35 lteq2d 
_1 = a1 : a2 -> (a3 < len _1 <-> a3 < len (a1 : a2))
37 34 appendeq1d 
_1 = a1 : a2 -> _1 ++ l2 = a1 : a2 ++ l2
38 37 ntheq2d 
_1 = a1 : a2 -> nth a3 (_1 ++ l2) = nth a3 (a1 : a2 ++ l2)
39 34 ntheq2d 
_1 = a1 : a2 -> nth a3 _1 = nth a3 (a1 : a2)
40 38, 39 eqeqd 
_1 = a1 : a2 -> (nth a3 (_1 ++ l2) = nth a3 _1 <-> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2))
41 36, 40 imeqd 
_1 = a1 : a2 -> (a3 < len _1 -> nth a3 (_1 ++ l2) = nth a3 _1 <-> a3 < len (a1 : a2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2))
42 41 aleqd 
_1 = a1 : a2 -> (A. a3 (a3 < len _1 -> nth a3 (_1 ++ l2) = nth a3 _1) <-> A. a3 (a3 < len (a1 : a2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2)))
43 lteq2 
len 0 = 0 -> (a3 < len 0 <-> a3 < 0)
44 len0 
len 0 = 0
45 43, 44 ax_mp 
a3 < len 0 <-> a3 < 0
46 absurd 
~a3 < 0 -> a3 < 0 -> nth a3 (0 ++ l2) = nth a3 0
47 lt02 
~a3 < 0
48 46, 47 ax_mp 
a3 < 0 -> nth a3 (0 ++ l2) = nth a3 0
49 45, 48 sylbi 
a3 < len 0 -> nth a3 (0 ++ l2) = nth a3 0
50 49 ax_gen 
A. a3 (a3 < len 0 -> nth a3 (0 ++ l2) = nth a3 0)
51 lteq1 
a3 = a4 -> (a3 < len a2 <-> a4 < len a2)
52 ntheq1 
a3 = a4 -> nth a3 (a2 ++ l2) = nth a4 (a2 ++ l2)
53 ntheq1 
a3 = a4 -> nth a3 a2 = nth a4 a2
54 52, 53 eqeqd 
a3 = a4 -> (nth a3 (a2 ++ l2) = nth a3 a2 <-> nth a4 (a2 ++ l2) = nth a4 a2)
55 51, 54 imeqd 
a3 = a4 -> (a3 < len a2 -> nth a3 (a2 ++ l2) = nth a3 a2 <-> a4 < len a2 -> nth a4 (a2 ++ l2) = nth a4 a2)
56 55 cbval 
A. a3 (a3 < len a2 -> nth a3 (a2 ++ l2) = nth a3 a2) <-> A. a4 (a4 < len a2 -> nth a4 (a2 ++ l2) = nth a4 a2)
57 ntheq2 
a1 : a2 ++ l2 = a1 : (a2 ++ l2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : (a2 ++ l2))
58 appendS 
a1 : a2 ++ l2 = a1 : (a2 ++ l2)
59 57, 58 ax_mp 
nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : (a2 ++ l2))
60 ntheq1 
a3 = 0 -> nth a3 (a1 : (a2 ++ l2)) = nth 0 (a1 : (a2 ++ l2))
61 eqtr4 
nth 0 (a1 : a2) = suc a1 -> nth 0 (a1 : (a2 ++ l2)) = suc a1 -> nth 0 (a1 : a2) = nth 0 (a1 : (a2 ++ l2))
62 nthZ 
nth 0 (a1 : a2) = suc a1
63 61, 62 ax_mp 
nth 0 (a1 : (a2 ++ l2)) = suc a1 -> nth 0 (a1 : a2) = nth 0 (a1 : (a2 ++ l2))
64 nthZ 
nth 0 (a1 : (a2 ++ l2)) = suc a1
65 63, 64 ax_mp 
nth 0 (a1 : a2) = nth 0 (a1 : (a2 ++ l2))
66 ntheq1 
a3 = 0 -> nth a3 (a1 : a2) = nth 0 (a1 : a2)
67 65, 66 syl6eq 
a3 = 0 -> nth a3 (a1 : a2) = nth 0 (a1 : (a2 ++ l2))
68 60, 67 eqtr4d 
a3 = 0 -> nth a3 (a1 : (a2 ++ l2)) = nth a3 (a1 : a2)
69 59, 68 syl5eq 
a3 = 0 -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2)
70 69 a1d 
a3 = 0 -> a3 < len (a1 : a2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2)
71 70 a1i 
A. a4 (a4 < len a2 -> nth a4 (a2 ++ l2) = nth a4 a2) -> a3 = 0 -> a3 < len (a1 : a2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2)
72 exsuc 
a3 != 0 <-> E. a4 a3 = suc a4
73 72 conv ne 
~a3 = 0 <-> E. a4 a3 = suc a4
74 eexb 
E. a4 a3 = suc a4 -> a3 < len (a1 : a2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2) <->
  A. a4 (a3 = suc a4 -> a3 < len (a1 : a2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2))
75 lteq2 
len (a1 : a2) = suc (len a2) -> (a3 < len (a1 : a2) <-> a3 < suc (len a2))
76 lenS 
len (a1 : a2) = suc (len a2)
77 75, 76 ax_mp 
a3 < len (a1 : a2) <-> a3 < suc (len a2)
78 ltsuc 
a4 < len a2 <-> suc a4 < suc (len a2)
79 lteq1 
a3 = suc a4 -> (a3 < suc (len a2) <-> suc a4 < suc (len a2))
80 78, 79 syl6bbr 
a3 = suc a4 -> (a3 < suc (len a2) <-> a4 < len a2)
81 77, 80 syl5bb 
a3 = suc a4 -> (a3 < len (a1 : a2) <-> a4 < len a2)
82 nthS 
nth (suc a4) (a1 : (a2 ++ l2)) = nth a4 (a2 ++ l2)
83 ntheq1 
a3 = suc a4 -> nth a3 (a1 : (a2 ++ l2)) = nth (suc a4) (a1 : (a2 ++ l2))
84 82, 83 syl6eq 
a3 = suc a4 -> nth a3 (a1 : (a2 ++ l2)) = nth a4 (a2 ++ l2)
85 59, 84 syl5eq 
a3 = suc a4 -> nth a3 (a1 : a2 ++ l2) = nth a4 (a2 ++ l2)
86 nthS 
nth (suc a4) (a1 : a2) = nth a4 a2
87 ntheq1 
a3 = suc a4 -> nth a3 (a1 : a2) = nth (suc a4) (a1 : a2)
88 86, 87 syl6eq 
a3 = suc a4 -> nth a3 (a1 : a2) = nth a4 a2
89 85, 88 eqeqd 
a3 = suc a4 -> (nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2) <-> nth a4 (a2 ++ l2) = nth a4 a2)
90 81, 89 imeqd 
a3 = suc a4 -> (a3 < len (a1 : a2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2) <-> a4 < len a2 -> nth a4 (a2 ++ l2) = nth a4 a2)
91 90 bi2d 
a3 = suc a4 -> (a4 < len a2 -> nth a4 (a2 ++ l2) = nth a4 a2) -> a3 < len (a1 : a2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2)
92 91 com12 
(a4 < len a2 -> nth a4 (a2 ++ l2) = nth a4 a2) -> a3 = suc a4 -> a3 < len (a1 : a2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2)
93 92 alimi 
A. a4 (a4 < len a2 -> nth a4 (a2 ++ l2) = nth a4 a2) -> A. a4 (a3 = suc a4 -> a3 < len (a1 : a2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2))
94 74, 93 sylibr 
A. a4 (a4 < len a2 -> nth a4 (a2 ++ l2) = nth a4 a2) -> E. a4 a3 = suc a4 -> a3 < len (a1 : a2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2)
95 73, 94 syl5bi 
A. a4 (a4 < len a2 -> nth a4 (a2 ++ l2) = nth a4 a2) -> ~a3 = 0 -> a3 < len (a1 : a2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2)
96 71, 95 casesd 
A. a4 (a4 < len a2 -> nth a4 (a2 ++ l2) = nth a4 a2) -> a3 < len (a1 : a2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2)
97 96 iald 
A. a4 (a4 < len a2 -> nth a4 (a2 ++ l2) = nth a4 a2) -> A. a3 (a3 < len (a1 : a2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2))
98 56, 97 sylbi 
A. a3 (a3 < len a2 -> nth a3 (a2 ++ l2) = nth a3 a2) -> A. a3 (a3 < len (a1 : a2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2))
99 15, 24, 33, 42, 50, 98 listind 
A. a3 (a3 < len l1 -> nth a3 (l1 ++ l2) = nth a3 l1)
100 6, 99 ax_mp 
i < len l1 -> nth i (l1 ++ l2) = nth i l1

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)