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 eqidd 
_1 = l1 -> a3 = a3
8 id 
_1 = l1 -> _1 = l1
9 8 leneqd 
_1 = l1 -> len _1 = len l1
10 7, 9 lteqd 
_1 = l1 -> (a3 < len _1 <-> a3 < len l1)
11 eqidd 
_1 = l1 -> l2 = l2
12 8, 11 appendeqd 
_1 = l1 -> _1 ++ l2 = l1 ++ l2
13 7, 12 ntheqd 
_1 = l1 -> nth a3 (_1 ++ l2) = nth a3 (l1 ++ l2)
14 7, 8 ntheqd 
_1 = l1 -> nth a3 _1 = nth a3 l1
15 13, 14 eqeqd 
_1 = l1 -> (nth a3 (_1 ++ l2) = nth a3 _1 <-> nth a3 (l1 ++ l2) = nth a3 l1)
16 10, 15 imeqd 
_1 = l1 -> (a3 < len _1 -> nth a3 (_1 ++ l2) = nth a3 _1 <-> a3 < len l1 -> nth a3 (l1 ++ l2) = nth a3 l1)
17 16 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))
18 eqidd 
_1 = 0 -> a3 = a3
19 id 
_1 = 0 -> _1 = 0
20 19 leneqd 
_1 = 0 -> len _1 = len 0
21 18, 20 lteqd 
_1 = 0 -> (a3 < len _1 <-> a3 < len 0)
22 eqidd 
_1 = 0 -> l2 = l2
23 19, 22 appendeqd 
_1 = 0 -> _1 ++ l2 = 0 ++ l2
24 18, 23 ntheqd 
_1 = 0 -> nth a3 (_1 ++ l2) = nth a3 (0 ++ l2)
25 18, 19 ntheqd 
_1 = 0 -> nth a3 _1 = nth a3 0
26 24, 25 eqeqd 
_1 = 0 -> (nth a3 (_1 ++ l2) = nth a3 _1 <-> nth a3 (0 ++ l2) = nth a3 0)
27 21, 26 imeqd 
_1 = 0 -> (a3 < len _1 -> nth a3 (_1 ++ l2) = nth a3 _1 <-> a3 < len 0 -> nth a3 (0 ++ l2) = nth a3 0)
28 27 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))
29 eqidd 
_1 = a2 -> a3 = a3
30 id 
_1 = a2 -> _1 = a2
31 30 leneqd 
_1 = a2 -> len _1 = len a2
32 29, 31 lteqd 
_1 = a2 -> (a3 < len _1 <-> a3 < len a2)
33 eqidd 
_1 = a2 -> l2 = l2
34 30, 33 appendeqd 
_1 = a2 -> _1 ++ l2 = a2 ++ l2
35 29, 34 ntheqd 
_1 = a2 -> nth a3 (_1 ++ l2) = nth a3 (a2 ++ l2)
36 29, 30 ntheqd 
_1 = a2 -> nth a3 _1 = nth a3 a2
37 35, 36 eqeqd 
_1 = a2 -> (nth a3 (_1 ++ l2) = nth a3 _1 <-> nth a3 (a2 ++ l2) = nth a3 a2)
38 32, 37 imeqd 
_1 = a2 -> (a3 < len _1 -> nth a3 (_1 ++ l2) = nth a3 _1 <-> a3 < len a2 -> nth a3 (a2 ++ l2) = nth a3 a2)
39 38 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))
40 eqidd 
_1 = a1 : a2 -> a3 = a3
41 id 
_1 = a1 : a2 -> _1 = a1 : a2
42 41 leneqd 
_1 = a1 : a2 -> len _1 = len (a1 : a2)
43 40, 42 lteqd 
_1 = a1 : a2 -> (a3 < len _1 <-> a3 < len (a1 : a2))
44 eqidd 
_1 = a1 : a2 -> l2 = l2
45 41, 44 appendeqd 
_1 = a1 : a2 -> _1 ++ l2 = a1 : a2 ++ l2
46 40, 45 ntheqd 
_1 = a1 : a2 -> nth a3 (_1 ++ l2) = nth a3 (a1 : a2 ++ l2)
47 40, 41 ntheqd 
_1 = a1 : a2 -> nth a3 _1 = nth a3 (a1 : a2)
48 46, 47 eqeqd 
_1 = a1 : a2 -> (nth a3 (_1 ++ l2) = nth a3 _1 <-> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2))
49 43, 48 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))
50 49 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)))
51 lteq2 
len 0 = 0 -> (a3 < len 0 <-> a3 < 0)
52 len0 
len 0 = 0
53 51, 52 ax_mp 
a3 < len 0 <-> a3 < 0
54 absurd 
~a3 < 0 -> a3 < 0 -> nth a3 (0 ++ l2) = nth a3 0
55 lt02 
~a3 < 0
56 54, 55 ax_mp 
a3 < 0 -> nth a3 (0 ++ l2) = nth a3 0
57 53, 56 sylbi 
a3 < len 0 -> nth a3 (0 ++ l2) = nth a3 0
58 57 ax_gen 
A. a3 (a3 < len 0 -> nth a3 (0 ++ l2) = nth a3 0)
59 lteq1 
a3 = a4 -> (a3 < len a2 <-> a4 < len a2)
60 ntheq1 
a3 = a4 -> nth a3 (a2 ++ l2) = nth a4 (a2 ++ l2)
61 ntheq1 
a3 = a4 -> nth a3 a2 = nth a4 a2
62 60, 61 eqeqd 
a3 = a4 -> (nth a3 (a2 ++ l2) = nth a3 a2 <-> nth a4 (a2 ++ l2) = nth a4 a2)
63 59, 62 imeqd 
a3 = a4 -> (a3 < len a2 -> nth a3 (a2 ++ l2) = nth a3 a2 <-> a4 < len a2 -> nth a4 (a2 ++ l2) = nth a4 a2)
64 63 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)
65 ntheq2 
a1 : a2 ++ l2 = a1 : (a2 ++ l2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : (a2 ++ l2))
66 appendS 
a1 : a2 ++ l2 = a1 : (a2 ++ l2)
67 65, 66 ax_mp 
nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : (a2 ++ l2))
68 ntheq1 
a3 = 0 -> nth a3 (a1 : (a2 ++ l2)) = nth 0 (a1 : (a2 ++ l2))
69 eqtr4 
nth 0 (a1 : a2) = suc a1 -> nth 0 (a1 : (a2 ++ l2)) = suc a1 -> nth 0 (a1 : a2) = nth 0 (a1 : (a2 ++ l2))
70 nthZ 
nth 0 (a1 : a2) = suc a1
71 69, 70 ax_mp 
nth 0 (a1 : (a2 ++ l2)) = suc a1 -> nth 0 (a1 : a2) = nth 0 (a1 : (a2 ++ l2))
72 nthZ 
nth 0 (a1 : (a2 ++ l2)) = suc a1
73 71, 72 ax_mp 
nth 0 (a1 : a2) = nth 0 (a1 : (a2 ++ l2))
74 ntheq1 
a3 = 0 -> nth a3 (a1 : a2) = nth 0 (a1 : a2)
75 73, 74 syl6eq 
a3 = 0 -> nth a3 (a1 : a2) = nth 0 (a1 : (a2 ++ l2))
76 68, 75 eqtr4d 
a3 = 0 -> nth a3 (a1 : (a2 ++ l2)) = nth a3 (a1 : a2)
77 67, 76 syl5eq 
a3 = 0 -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2)
78 77 a1d 
a3 = 0 -> a3 < len (a1 : a2) -> nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2)
79 78 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)
80 exsuc 
a3 != 0 <-> E. a4 a3 = suc a4
81 80 conv ne 
~a3 = 0 <-> E. a4 a3 = suc a4
82 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))
83 lteq2 
len (a1 : a2) = suc (len a2) -> (a3 < len (a1 : a2) <-> a3 < suc (len a2))
84 lenS 
len (a1 : a2) = suc (len a2)
85 83, 84 ax_mp 
a3 < len (a1 : a2) <-> a3 < suc (len a2)
86 ltsuc 
a4 < len a2 <-> suc a4 < suc (len a2)
87 lteq1 
a3 = suc a4 -> (a3 < suc (len a2) <-> suc a4 < suc (len a2))
88 86, 87 syl6bbr 
a3 = suc a4 -> (a3 < suc (len a2) <-> a4 < len a2)
89 85, 88 syl5bb 
a3 = suc a4 -> (a3 < len (a1 : a2) <-> a4 < len a2)
90 nthS 
nth (suc a4) (a1 : (a2 ++ l2)) = nth a4 (a2 ++ l2)
91 ntheq1 
a3 = suc a4 -> nth a3 (a1 : (a2 ++ l2)) = nth (suc a4) (a1 : (a2 ++ l2))
92 90, 91 syl6eq 
a3 = suc a4 -> nth a3 (a1 : (a2 ++ l2)) = nth a4 (a2 ++ l2)
93 67, 92 syl5eq 
a3 = suc a4 -> nth a3 (a1 : a2 ++ l2) = nth a4 (a2 ++ l2)
94 nthS 
nth (suc a4) (a1 : a2) = nth a4 a2
95 ntheq1 
a3 = suc a4 -> nth a3 (a1 : a2) = nth (suc a4) (a1 : a2)
96 94, 95 syl6eq 
a3 = suc a4 -> nth a3 (a1 : a2) = nth a4 a2
97 93, 96 eqeqd 
a3 = suc a4 -> (nth a3 (a1 : a2 ++ l2) = nth a3 (a1 : a2) <-> nth a4 (a2 ++ l2) = nth a4 a2)
98 89, 97 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)
99 98 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)
100 99 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)
101 100 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))
102 82, 101 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)
103 81, 102 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)
104 79, 103 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)
105 104 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))
106 64, 105 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))
107 17, 28, 39, 50, 58, 106 listind 
A. a3 (a3 < len l1 -> nth a3 (l1 ++ l2) = nth a3 l1)
108 6, 107 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)