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