Theorem appendlen ≪ | index | src | ≫ 

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