Theorem appendlen ≪ | index | src | ≫ 

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