Theorem appendnth2_ ≪ | index | src | ≫ 

theorem appendnth2_ (i l1 l2: nat): $ nth (len l1 + i) (l1 ++ l2) = nth i l2 $;
StepHypRefExpression
1 id 
_1 = l1 -> _1 = l1
2 1 leneqd 
_1 = l1 -> len _1 = len l1
3 eqidd 
_1 = l1 -> i = i
4 2, 3 addeqd 
_1 = l1 -> len _1 + i = len l1 + i
5 eqidd 
_1 = l1 -> l2 = l2
6 1, 5 appendeqd 
_1 = l1 -> _1 ++ l2 = l1 ++ l2
7 4, 6 ntheqd 
_1 = l1 -> nth (len _1 + i) (_1 ++ l2) = nth (len l1 + i) (l1 ++ l2)
8 eqidd 
_1 = l1 -> nth i l2 = nth i l2
9 7, 8 eqeqd 
_1 = l1 -> (nth (len _1 + i) (_1 ++ l2) = nth i l2 <-> nth (len l1 + i) (l1 ++ l2) = nth i l2)
10 id 
_1 = 0 -> _1 = 0
11 10 leneqd 
_1 = 0 -> len _1 = len 0
12 eqidd 
_1 = 0 -> i = i
13 11, 12 addeqd 
_1 = 0 -> len _1 + i = len 0 + i
14 eqidd 
_1 = 0 -> l2 = l2
15 10, 14 appendeqd 
_1 = 0 -> _1 ++ l2 = 0 ++ l2
16 13, 15 ntheqd 
_1 = 0 -> nth (len _1 + i) (_1 ++ l2) = nth (len 0 + i) (0 ++ l2)
17 eqidd 
_1 = 0 -> nth i l2 = nth i l2
18 16, 17 eqeqd 
_1 = 0 -> (nth (len _1 + i) (_1 ++ l2) = nth i l2 <-> nth (len 0 + i) (0 ++ l2) = nth i l2)
19 id 
_1 = a2 -> _1 = a2
20 19 leneqd 
_1 = a2 -> len _1 = len a2
21 eqidd 
_1 = a2 -> i = i
22 20, 21 addeqd 
_1 = a2 -> len _1 + i = len a2 + i
23 eqidd 
_1 = a2 -> l2 = l2
24 19, 23 appendeqd 
_1 = a2 -> _1 ++ l2 = a2 ++ l2
25 22, 24 ntheqd 
_1 = a2 -> nth (len _1 + i) (_1 ++ l2) = nth (len a2 + i) (a2 ++ l2)
26 eqidd 
_1 = a2 -> nth i l2 = nth i l2
27 25, 26 eqeqd 
_1 = a2 -> (nth (len _1 + i) (_1 ++ l2) = nth i l2 <-> nth (len a2 + i) (a2 ++ l2) = nth i l2)
28 id 
_1 = a1 : a2 -> _1 = a1 : a2
29 28 leneqd 
_1 = a1 : a2 -> len _1 = len (a1 : a2)
30 eqidd 
_1 = a1 : a2 -> i = i
31 29, 30 addeqd 
_1 = a1 : a2 -> len _1 + i = len (a1 : a2) + i
32 eqidd 
_1 = a1 : a2 -> l2 = l2
33 28, 32 appendeqd 
_1 = a1 : a2 -> _1 ++ l2 = a1 : a2 ++ l2
34 31, 33 ntheqd 
_1 = a1 : a2 -> nth (len _1 + i) (_1 ++ l2) = nth (len (a1 : a2) + i) (a1 : a2 ++ l2)
35 eqidd 
_1 = a1 : a2 -> nth i l2 = nth i l2
36 34, 35 eqeqd 
_1 = a1 : a2 -> (nth (len _1 + i) (_1 ++ l2) = nth i l2 <-> nth (len (a1 : a2) + i) (a1 : a2 ++ l2) = nth i l2)
37 ntheq 
len 0 + i = i -> 0 ++ l2 = l2 -> nth (len 0 + i) (0 ++ l2) = nth i l2
38 eqtr 
len 0 + i = 0 + i -> 0 + i = i -> len 0 + i = i
39 addeq1 
len 0 = 0 -> len 0 + i = 0 + i
40 len0 
len 0 = 0
41 39, 40 ax_mp 
len 0 + i = 0 + i
42 38, 41 ax_mp 
0 + i = i -> len 0 + i = i
43 add01 
0 + i = i
44 42, 43 ax_mp 
len 0 + i = i
45 37, 44 ax_mp 
0 ++ l2 = l2 -> nth (len 0 + i) (0 ++ l2) = nth i l2
46 append0 
0 ++ l2 = l2
47 45, 46 ax_mp 
nth (len 0 + i) (0 ++ l2) = nth i l2
48 eqtr 
nth (len (a1 : a2) + i) (a1 : a2 ++ l2) = nth (suc (len a2 + i)) (a1 : (a2 ++ l2)) ->
  nth (suc (len a2 + i)) (a1 : (a2 ++ l2)) = nth (len a2 + i) (a2 ++ l2) ->
  nth (len (a1 : a2) + i) (a1 : a2 ++ l2) = nth (len a2 + i) (a2 ++ l2)
49 ntheq 
len (a1 : a2) + i = suc (len a2 + i) -> a1 : a2 ++ l2 = a1 : (a2 ++ l2) -> nth (len (a1 : a2) + i) (a1 : a2 ++ l2) = nth (suc (len a2 + i)) (a1 : (a2 ++ l2))
50 eqtr 
len (a1 : a2) + i = suc (len a2) + i -> suc (len a2) + i = suc (len a2 + i) -> len (a1 : a2) + i = suc (len a2 + i)
51 addeq1 
len (a1 : a2) = suc (len a2) -> len (a1 : a2) + i = suc (len a2) + i
52 lenS 
len (a1 : a2) = suc (len a2)
53 51, 52 ax_mp 
len (a1 : a2) + i = suc (len a2) + i
54 50, 53 ax_mp 
suc (len a2) + i = suc (len a2 + i) -> len (a1 : a2) + i = suc (len a2 + i)
55 addS1 
suc (len a2) + i = suc (len a2 + i)
56 54, 55 ax_mp 
len (a1 : a2) + i = suc (len a2 + i)
57 49, 56 ax_mp 
a1 : a2 ++ l2 = a1 : (a2 ++ l2) -> nth (len (a1 : a2) + i) (a1 : a2 ++ l2) = nth (suc (len a2 + i)) (a1 : (a2 ++ l2))
58 appendS 
a1 : a2 ++ l2 = a1 : (a2 ++ l2)
59 57, 58 ax_mp 
nth (len (a1 : a2) + i) (a1 : a2 ++ l2) = nth (suc (len a2 + i)) (a1 : (a2 ++ l2))
60 48, 59 ax_mp 
nth (suc (len a2 + i)) (a1 : (a2 ++ l2)) = nth (len a2 + i) (a2 ++ l2) -> nth (len (a1 : a2) + i) (a1 : a2 ++ l2) = nth (len a2 + i) (a2 ++ l2)
61 nthS 
nth (suc (len a2 + i)) (a1 : (a2 ++ l2)) = nth (len a2 + i) (a2 ++ l2)
62 60, 61 ax_mp 
nth (len (a1 : a2) + i) (a1 : a2 ++ l2) = nth (len a2 + i) (a2 ++ l2)
63 id 
nth (len a2 + i) (a2 ++ l2) = nth i l2 -> nth (len a2 + i) (a2 ++ l2) = nth i l2
64 62, 63 syl5eq 
nth (len a2 + i) (a2 ++ l2) = nth i l2 -> nth (len (a1 : a2) + i) (a1 : a2 ++ l2) = nth i l2
65 9, 18, 27, 36, 47, 64 listind 
nth (len l1 + i) (l1 ++ l2) = nth i l2

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)