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 2 addeq1d 
_1 = l1 -> len _1 + i = len l1 + i
4 1 appendeq1d 
_1 = l1 -> _1 ++ l2 = l1 ++ l2
5 3, 4 ntheqd 
_1 = l1 -> nth (len _1 + i) (_1 ++ l2) = nth (len l1 + i) (l1 ++ l2)
6 5 eqeq1d 
_1 = l1 -> (nth (len _1 + i) (_1 ++ l2) = nth i l2 <-> nth (len l1 + i) (l1 ++ l2) = nth i l2)
7 id 
_1 = 0 -> _1 = 0
8 7 leneqd 
_1 = 0 -> len _1 = len 0
9 8 addeq1d 
_1 = 0 -> len _1 + i = len 0 + i
10 7 appendeq1d 
_1 = 0 -> _1 ++ l2 = 0 ++ l2
11 9, 10 ntheqd 
_1 = 0 -> nth (len _1 + i) (_1 ++ l2) = nth (len 0 + i) (0 ++ l2)
12 11 eqeq1d 
_1 = 0 -> (nth (len _1 + i) (_1 ++ l2) = nth i l2 <-> nth (len 0 + i) (0 ++ l2) = nth i l2)
13 id 
_1 = a2 -> _1 = a2
14 13 leneqd 
_1 = a2 -> len _1 = len a2
15 14 addeq1d 
_1 = a2 -> len _1 + i = len a2 + i
16 13 appendeq1d 
_1 = a2 -> _1 ++ l2 = a2 ++ l2
17 15, 16 ntheqd 
_1 = a2 -> nth (len _1 + i) (_1 ++ l2) = nth (len a2 + i) (a2 ++ l2)
18 17 eqeq1d 
_1 = a2 -> (nth (len _1 + i) (_1 ++ l2) = nth i l2 <-> nth (len a2 + i) (a2 ++ l2) = nth i l2)
19 id 
_1 = a1 : a2 -> _1 = a1 : a2
20 19 leneqd 
_1 = a1 : a2 -> len _1 = len (a1 : a2)
21 20 addeq1d 
_1 = a1 : a2 -> len _1 + i = len (a1 : a2) + i
22 19 appendeq1d 
_1 = a1 : a2 -> _1 ++ l2 = a1 : a2 ++ l2
23 21, 22 ntheqd 
_1 = a1 : a2 -> nth (len _1 + i) (_1 ++ l2) = nth (len (a1 : a2) + i) (a1 : a2 ++ l2)
24 23 eqeq1d 
_1 = a1 : a2 -> (nth (len _1 + i) (_1 ++ l2) = nth i l2 <-> nth (len (a1 : a2) + i) (a1 : a2 ++ l2) = nth i l2)
25 ntheq 
len 0 + i = i -> 0 ++ l2 = l2 -> nth (len 0 + i) (0 ++ l2) = nth i l2
26 eqtr 
len 0 + i = 0 + i -> 0 + i = i -> len 0 + i = i
27 addeq1 
len 0 = 0 -> len 0 + i = 0 + i
28 len0 
len 0 = 0
29 27, 28 ax_mp 
len 0 + i = 0 + i
30 26, 29 ax_mp 
0 + i = i -> len 0 + i = i
31 add01 
0 + i = i
32 30, 31 ax_mp 
len 0 + i = i
33 25, 32 ax_mp 
0 ++ l2 = l2 -> nth (len 0 + i) (0 ++ l2) = nth i l2
34 append0 
0 ++ l2 = l2
35 33, 34 ax_mp 
nth (len 0 + i) (0 ++ l2) = nth i l2
36 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)
37 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))
38 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)
39 addeq1 
len (a1 : a2) = suc (len a2) -> len (a1 : a2) + i = suc (len a2) + i
40 lenS 
len (a1 : a2) = suc (len a2)
41 39, 40 ax_mp 
len (a1 : a2) + i = suc (len a2) + i
42 38, 41 ax_mp 
suc (len a2) + i = suc (len a2 + i) -> len (a1 : a2) + i = suc (len a2 + i)
43 addS1 
suc (len a2) + i = suc (len a2 + i)
44 42, 43 ax_mp 
len (a1 : a2) + i = suc (len a2 + i)
45 37, 44 ax_mp 
a1 : a2 ++ l2 = a1 : (a2 ++ l2) -> nth (len (a1 : a2) + i) (a1 : a2 ++ l2) = nth (suc (len a2 + i)) (a1 : (a2 ++ l2))
46 appendS 
a1 : a2 ++ l2 = a1 : (a2 ++ l2)
47 45, 46 ax_mp 
nth (len (a1 : a2) + i) (a1 : a2 ++ l2) = nth (suc (len a2 + i)) (a1 : (a2 ++ l2))
48 36, 47 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)
49 nthS 
nth (suc (len a2 + i)) (a1 : (a2 ++ l2)) = nth (len a2 + i) (a2 ++ l2)
50 48, 49 ax_mp 
nth (len (a1 : a2) + i) (a1 : a2 ++ l2) = nth (len a2 + i) (a2 ++ l2)
51 id 
nth (len a2 + i) (a2 ++ l2) = nth i l2 -> nth (len a2 + i) (a2 ++ l2) = nth i l2
52 50, 51 syl5eq 
nth (len a2 + i) (a2 ++ l2) = nth i l2 -> nth (len (a1 : a2) + i) (a1 : a2 ++ l2) = nth i l2
53 6, 12, 18, 24, 35, 52 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)