Theorem repeatlen ≪ | index | src | ≫

theorem repeatlen (a n: nat): $ len (repeat a n) = n $;


_1 = n -> _1 = n
_1 = n -> repeat a _1 = repeat a n
_1 = n -> len (repeat a _1) = len (repeat a n)
_1 = n -> (len (repeat a _1) = _1 <-> len (repeat a n) = n)
_1 = 0 -> _1 = 0
_1 = 0 -> repeat a _1 = repeat a 0
_1 = 0 -> len (repeat a _1) = len (repeat a 0)
_1 = 0 -> (len (repeat a _1) = _1 <-> len (repeat a 0) = 0)
_1 = a1 -> _1 = a1
_1 = a1 -> repeat a _1 = repeat a a1
_1 = a1 -> len (repeat a _1) = len (repeat a a1)
_1 = a1 -> (len (repeat a _1) = _1 <-> len (repeat a a1) = a1)
_1 = suc a1 -> _1 = suc a1
_1 = suc a1 -> repeat a _1 = repeat a (suc a1)
_1 = suc a1 -> len (repeat a _1) = len (repeat a (suc a1))
_1 = suc a1 -> (len (repeat a _1) = _1 <-> len (repeat a (suc a1)) = suc a1)
len (repeat a 0) = len 0 -> len 0 = 0 -> len (repeat a 0) = 0
repeat a 0 = 0 -> len (repeat a 0) = len 0
repeat a 0 = 0
len (repeat a 0) = len 0
len 0 = 0 -> len (repeat a 0) = 0
len 0 = 0
len (repeat a 0) = 0
repeat a (suc a1) = a : repeat a a1 -> len (repeat a (suc a1)) = len (a : repeat a a1)
repeat a (suc a1) = a : repeat a a1
len (repeat a (suc a1)) = len (a : repeat a a1)
len (a : repeat a a1) = suc (len (repeat a a1))
len (repeat a a1) = a1 -> suc (len (repeat a a1)) = suc a1
len (repeat a a1) = a1 -> len (a : repeat a a1) = suc a1
len (repeat a a1) = a1 -> len (repeat a (suc a1)) = suc a1
len (repeat a n) = n

Step	Hyp	Ref	Expression
1		id	_1 = n -> _1 = n
2	1	repeateq2d	_1 = n -> repeat a _1 = repeat a n
3	2	leneqd	_1 = n -> len (repeat a _1) = len (repeat a n)
4	3, 1	eqeqd	_1 = n -> (len (repeat a _1) = _1 <-> len (repeat a n) = n)
5		id	_1 = 0 -> _1 = 0
6	5	repeateq2d	_1 = 0 -> repeat a _1 = repeat a 0
7	6	leneqd	_1 = 0 -> len (repeat a _1) = len (repeat a 0)
8	7, 5	eqeqd	_1 = 0 -> (len (repeat a _1) = _1 <-> len (repeat a 0) = 0)
9		id	_1 = a1 -> _1 = a1
10	9	repeateq2d	_1 = a1 -> repeat a _1 = repeat a a1
11	10	leneqd	_1 = a1 -> len (repeat a _1) = len (repeat a a1)
12	11, 9	eqeqd	_1 = a1 -> (len (repeat a _1) = _1 <-> len (repeat a a1) = a1)
13		id	_1 = suc a1 -> _1 = suc a1
14	13	repeateq2d	_1 = suc a1 -> repeat a _1 = repeat a (suc a1)
15	14	leneqd	_1 = suc a1 -> len (repeat a _1) = len (repeat a (suc a1))
16	15, 13	eqeqd	_1 = suc a1 -> (len (repeat a _1) = _1 <-> len (repeat a (suc a1)) = suc a1)
17		eqtr	len (repeat a 0) = len 0 -> len 0 = 0 -> len (repeat a 0) = 0
18		leneq	repeat a 0 = 0 -> len (repeat a 0) = len 0
19		repeat0	repeat a 0 = 0
20	18, 19	ax_mp	len (repeat a 0) = len 0
21	17, 20	ax_mp	len 0 = 0 -> len (repeat a 0) = 0
22		len0	len 0 = 0
23	21, 22	ax_mp	len (repeat a 0) = 0
24		leneq	repeat a (suc a1) = a : repeat a a1 -> len (repeat a (suc a1)) = len (a : repeat a a1)
25		repeatS	repeat a (suc a1) = a : repeat a a1
26	24, 25	ax_mp	len (repeat a (suc a1)) = len (a : repeat a a1)
27		lenS	len (a : repeat a a1) = suc (len (repeat a a1))
28		suceq	len (repeat a a1) = a1 -> suc (len (repeat a a1)) = suc a1
29	27, 28	syl5eq	len (repeat a a1) = a1 -> len (a : repeat a a1) = suc a1
30	26, 29	syl5eq	len (repeat a a1) = a1 -> len (repeat a (suc a1)) = suc a1
31	4, 8, 12, 16, 23, 30	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)