Theorem repeatlen ≪ | index | src | ≫ 

theorem repeatlen (a n: nat): $ len (repeat a n) = n $;
StepHypRefExpression
1 eqidd 
_1 = n -> a = a
2 id 
_1 = n -> _1 = n
3 1, 2 repeateqd 
_1 = n -> repeat a _1 = repeat a n
4 3 leneqd 
_1 = n -> len (repeat a _1) = len (repeat a n)
5 4, 2 eqeqd 
_1 = n -> (len (repeat a _1) = _1 <-> len (repeat a n) = n)
6 eqidd 
_1 = 0 -> a = a
7 id 
_1 = 0 -> _1 = 0
8 6, 7 repeateqd 
_1 = 0 -> repeat a _1 = repeat a 0
9 8 leneqd 
_1 = 0 -> len (repeat a _1) = len (repeat a 0)
10 9, 7 eqeqd 
_1 = 0 -> (len (repeat a _1) = _1 <-> len (repeat a 0) = 0)
11 eqidd 
_1 = a1 -> a = a
12 id 
_1 = a1 -> _1 = a1
13 11, 12 repeateqd 
_1 = a1 -> repeat a _1 = repeat a a1
14 13 leneqd 
_1 = a1 -> len (repeat a _1) = len (repeat a a1)
15 14, 12 eqeqd 
_1 = a1 -> (len (repeat a _1) = _1 <-> len (repeat a a1) = a1)
16 eqidd 
_1 = suc a1 -> a = a
17 id 
_1 = suc a1 -> _1 = suc a1
18 16, 17 repeateqd 
_1 = suc a1 -> repeat a _1 = repeat a (suc a1)
19 18 leneqd 
_1 = suc a1 -> len (repeat a _1) = len (repeat a (suc a1))
20 19, 17 eqeqd 
_1 = suc a1 -> (len (repeat a _1) = _1 <-> len (repeat a (suc a1)) = suc a1)
21 eqtr 
len (repeat a 0) = len 0 -> len 0 = 0 -> len (repeat a 0) = 0
22 leneq 
repeat a 0 = 0 -> len (repeat a 0) = len 0
23 repeat0 
repeat a 0 = 0
24 22, 23 ax_mp 
len (repeat a 0) = len 0
25 21, 24 ax_mp 
len 0 = 0 -> len (repeat a 0) = 0
26 len0 
len 0 = 0
27 25, 26 ax_mp 
len (repeat a 0) = 0
28 leneq 
repeat a (suc a1) = a : repeat a a1 -> len (repeat a (suc a1)) = len (a : repeat a a1)
29 repeatS 
repeat a (suc a1) = a : repeat a a1
30 28, 29 ax_mp 
len (repeat a (suc a1)) = len (a : repeat a a1)
31 lenS 
len (a : repeat a a1) = suc (len (repeat a a1))
32 suceq 
len (repeat a a1) = a1 -> suc (len (repeat a a1)) = suc a1
33 31, 32 syl5eq 
len (repeat a a1) = a1 -> len (a : repeat a a1) = suc a1
34 30, 33 syl5eq 
len (repeat a a1) = a1 -> len (repeat a (suc a1)) = suc a1
35 5, 10, 15, 20, 27, 34 ind 
len (repeat a n) = n

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)