Theorem lfnauxlen ≪ | index | src | ≫

theorem lfnauxlen (F: set) (k n: nat): $ len (lfnaux F k n) = n $;

Step	Hyp	Ref	Expression
1		lfnauxeq2	a2 = k -> lfnaux F a2 n = lfnaux F k n
2	1	leneqd	a2 = k -> len (lfnaux F a2 n) = len (lfnaux F k n)
3	2	eqeq1d	a2 = k -> (len (lfnaux F a2 n) = n <-> len (lfnaux F k n) = n)
4	3	eale	A. a2 len (lfnaux F a2 n) = n -> len (lfnaux F k n) = n
5		id	_1 = n -> _1 = n
6	5	lfnauxeq3d	_1 = n -> lfnaux F a2 _1 = lfnaux F a2 n
7	6	leneqd	_1 = n -> len (lfnaux F a2 _1) = len (lfnaux F a2 n)
8	7, 5	eqeqd	_1 = n -> (len (lfnaux F a2 _1) = _1 <-> len (lfnaux F a2 n) = n)
9	8	aleqd	_1 = n -> (A. a2 len (lfnaux F a2 _1) = _1 <-> A. a2 len (lfnaux F a2 n) = n)
10		id	_1 = 0 -> _1 = 0
11	10	lfnauxeq3d	_1 = 0 -> lfnaux F a2 _1 = lfnaux F a2 0
12	11	leneqd	_1 = 0 -> len (lfnaux F a2 _1) = len (lfnaux F a2 0)
13	12, 10	eqeqd	_1 = 0 -> (len (lfnaux F a2 _1) = _1 <-> len (lfnaux F a2 0) = 0)
14	13	aleqd	_1 = 0 -> (A. a2 len (lfnaux F a2 _1) = _1 <-> A. a2 len (lfnaux F a2 0) = 0)
15		id	_1 = a1 -> _1 = a1
16	15	lfnauxeq3d	_1 = a1 -> lfnaux F a2 _1 = lfnaux F a2 a1
17	16	leneqd	_1 = a1 -> len (lfnaux F a2 _1) = len (lfnaux F a2 a1)
18	17, 15	eqeqd	_1 = a1 -> (len (lfnaux F a2 _1) = _1 <-> len (lfnaux F a2 a1) = a1)
19	18	aleqd	_1 = a1 -> (A. a2 len (lfnaux F a2 _1) = _1 <-> A. a2 len (lfnaux F a2 a1) = a1)
20		id	_1 = suc a1 -> _1 = suc a1
21	20	lfnauxeq3d	_1 = suc a1 -> lfnaux F a2 _1 = lfnaux F a2 (suc a1)
22	21	leneqd	_1 = suc a1 -> len (lfnaux F a2 _1) = len (lfnaux F a2 (suc a1))
23	22, 20	eqeqd	_1 = suc a1 -> (len (lfnaux F a2 _1) = _1 <-> len (lfnaux F a2 (suc a1)) = suc a1)
24	23	aleqd	_1 = suc a1 -> (A. a2 len (lfnaux F a2 _1) = _1 <-> A. a2 len (lfnaux F a2 (suc a1)) = suc a1)
25		eqtr	len (lfnaux F a2 0) = len 0 -> len 0 = 0 -> len (lfnaux F a2 0) = 0
26		leneq	lfnaux F a2 0 = 0 -> len (lfnaux F a2 0) = len 0
27		lfnaux0	lfnaux F a2 0 = 0
28	26, 27	ax_mp	len (lfnaux F a2 0) = len 0
29	25, 28	ax_mp	len 0 = 0 -> len (lfnaux F a2 0) = 0
30		len0	len 0 = 0
31	29, 30	ax_mp	len (lfnaux F a2 0) = 0
32	31	ax_gen	A. a2 len (lfnaux F a2 0) = 0
33		lfnauxeq2	a2 = a3 -> lfnaux F a2 a1 = lfnaux F a3 a1
34	33	leneqd	a2 = a3 -> len (lfnaux F a2 a1) = len (lfnaux F a3 a1)
35	34	eqeq1d	a2 = a3 -> (len (lfnaux F a2 a1) = a1 <-> len (lfnaux F a3 a1) = a1)
36	35	cbval	A. a2 len (lfnaux F a2 a1) = a1 <-> A. a3 len (lfnaux F a3 a1) = a1
37		leneq	lfnaux F a2 (suc a1) = F @ a2 : lfnaux F (suc a2) a1 -> len (lfnaux F a2 (suc a1)) = len (F @ a2 : lfnaux F (suc a2) a1)
38		lfnauxS	lfnaux F a2 (suc a1) = F @ a2 : lfnaux F (suc a2) a1
39	37, 38	ax_mp	len (lfnaux F a2 (suc a1)) = len (F @ a2 : lfnaux F (suc a2) a1)
40		lenS	len (F @ a2 : lfnaux F (suc a2) a1) = suc (len (lfnaux F (suc a2) a1))
41		lfnauxeq2	a3 = suc a2 -> lfnaux F a3 a1 = lfnaux F (suc a2) a1
42	41	leneqd	a3 = suc a2 -> len (lfnaux F a3 a1) = len (lfnaux F (suc a2) a1)
43	42	eqeq1d	a3 = suc a2 -> (len (lfnaux F a3 a1) = a1 <-> len (lfnaux F (suc a2) a1) = a1)
44	43	eale	A. a3 len (lfnaux F a3 a1) = a1 -> len (lfnaux F (suc a2) a1) = a1
45	44	suceqd	A. a3 len (lfnaux F a3 a1) = a1 -> suc (len (lfnaux F (suc a2) a1)) = suc a1
46	40, 45	syl5eq	A. a3 len (lfnaux F a3 a1) = a1 -> len (F @ a2 : lfnaux F (suc a2) a1) = suc a1
47	39, 46	syl5eq	A. a3 len (lfnaux F a3 a1) = a1 -> len (lfnaux F a2 (suc a1)) = suc a1
48	47	iald	A. a3 len (lfnaux F a3 a1) = a1 -> A. a2 len (lfnaux F a2 (suc a1)) = suc a1
49	36, 48	sylbi	A. a2 len (lfnaux F a2 a1) = a1 -> A. a2 len (lfnaux F a2 (suc a1)) = suc a1
50	9, 14, 19, 24, 32, 49	ind	A. a2 len (lfnaux F a2 n) = n
51	4, 50	ax_mp	len (lfnaux F k 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)