lfnauxnth - examples/peano.mm1

Step	Hyp	Ref	Expression
1		anl	a2 = i /\ a3 = k -> a2 = i
2	1	lteq1d	a2 = i /\ a3 = k -> (a2 < n <-> i < n)
3		anr	a2 = i /\ a3 = k -> a3 = k
4	3	lfnauxeq2d	a2 = i /\ a3 = k -> lfnaux F a3 n = lfnaux F k n
5	1, 4	ntheqd	a2 = i /\ a3 = k -> nth a2 (lfnaux F a3 n) = nth i (lfnaux F k n)
6	3, 1	addeqd	a2 = i /\ a3 = k -> a3 + a2 = k + i
7	6	appeq2d	a2 = i /\ a3 = k -> F @ (a3 + a2) = F @ (k + i)
8	7	suceqd	a2 = i /\ a3 = k -> suc (F @ (a3 + a2)) = suc (F @ (k + i))
9	5, 8	eqeqd	a2 = i /\ a3 = k -> (nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)) <-> nth i (lfnaux F k n) = suc (F @ (k + i)))
10	2, 9	imeqd	a2 = i /\ a3 = k -> (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)) <-> i < n -> nth i (lfnaux F k n) = suc (F @ (k + i)))
11	10	bi1d	a2 = i /\ a3 = k -> (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))) -> i < n -> nth i (lfnaux F k n) = suc (F @ (k + i))
12	11	ealde	a2 = i -> A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))) -> i < n -> nth i (lfnaux F k n) = suc (F @ (k + i))
13	12	ealie	A. a2 A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))) -> i < n -> nth i (lfnaux F k n) = suc (F @ (k + i))
14		id	_1 = n -> _1 = n
15	14	lteq2d	_1 = n -> (a2 < _1 <-> a2 < n)
16	14	lfnauxeq3d	_1 = n -> lfnaux F a3 _1 = lfnaux F a3 n
17	16	ntheq2d	_1 = n -> nth a2 (lfnaux F a3 _1) = nth a2 (lfnaux F a3 n)
18	17	eqeq1d	_1 = n -> (nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)))
19	15, 18	imeqd	_1 = n -> (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)))
20	19	aleqd	_1 = n -> (A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))))
21	20	aleqd	_1 = n -> (A. a2 A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a2 A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))))
22		id	_1 = 0 -> _1 = 0
23	22	lteq2d	_1 = 0 -> (a2 < _1 <-> a2 < 0)
24	22	lfnauxeq3d	_1 = 0 -> lfnaux F a3 _1 = lfnaux F a3 0
25	24	ntheq2d	_1 = 0 -> nth a2 (lfnaux F a3 _1) = nth a2 (lfnaux F a3 0)
26	25	eqeq1d	_1 = 0 -> (nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2)))
27	23, 26	imeqd	_1 = 0 -> (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2)))
28	27	aleqd	_1 = 0 -> (A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a3 (a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2))))
29	28	aleqd	_1 = 0 -> (A. a2 A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a2 A. a3 (a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2))))
30		id	_1 = a1 -> _1 = a1
31	30	lteq2d	_1 = a1 -> (a2 < _1 <-> a2 < a1)
32	30	lfnauxeq3d	_1 = a1 -> lfnaux F a3 _1 = lfnaux F a3 a1
33	32	ntheq2d	_1 = a1 -> nth a2 (lfnaux F a3 _1) = nth a2 (lfnaux F a3 a1)
34	33	eqeq1d	_1 = a1 -> (nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2)))
35	31, 34	imeqd	_1 = a1 -> (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2)))
36	35	aleqd	_1 = a1 -> (A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))))
37	36	aleqd	_1 = a1 -> (A. a2 A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a2 A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))))
38		id	_1 = suc a1 -> _1 = suc a1
39	38	lteq2d	_1 = suc a1 -> (a2 < _1 <-> a2 < suc a1)
40	38	lfnauxeq3d	_1 = suc a1 -> lfnaux F a3 _1 = lfnaux F a3 (suc a1)
41	40	ntheq2d	_1 = suc a1 -> nth a2 (lfnaux F a3 _1) = nth a2 (lfnaux F a3 (suc a1))
42	41	eqeq1d	_1 = suc a1 -> (nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))
43	39, 42	imeqd	_1 = suc a1 -> (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))
44	43	aleqd	_1 = suc a1 -> (A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2))))
45	44	aleqd	_1 = suc a1 -> (A. a2 A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a2 A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2))))
46		absurd	~a2 < 0 -> a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2))
47		lt02	~a2 < 0
48	46, 47	ax_mp	a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2))
49	48	ax_gen	A. a3 (a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2)))
50	49	ax_gen	A. a2 A. a3 (a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2)))
51		anl	a2 = a4 /\ a3 = a5 -> a2 = a4
52	51	lteq1d	a2 = a4 /\ a3 = a5 -> (a2 < a1 <-> a4 < a1)
53		anr	a2 = a4 /\ a3 = a5 -> a3 = a5
54	53	lfnauxeq2d	a2 = a4 /\ a3 = a5 -> lfnaux F a3 a1 = lfnaux F a5 a1
55	51, 54	ntheqd	a2 = a4 /\ a3 = a5 -> nth a2 (lfnaux F a3 a1) = nth a4 (lfnaux F a5 a1)
56	53, 51	addeqd	a2 = a4 /\ a3 = a5 -> a3 + a2 = a5 + a4
57	56	appeq2d	a2 = a4 /\ a3 = a5 -> F @ (a3 + a2) = F @ (a5 + a4)
58	57	suceqd	a2 = a4 /\ a3 = a5 -> suc (F @ (a3 + a2)) = suc (F @ (a5 + a4))
59	55, 58	eqeqd	a2 = a4 /\ a3 = a5 -> (nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2)) <-> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))
60	52, 59	imeqd	a2 = a4 /\ a3 = a5 -> (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2)) <-> a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))
61	60	cbvald	a2 = a4 -> (A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))) <-> A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))))
62	61	cbval	A. a2 A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))) <-> A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))
63		ntheq2	lfnaux F a3 (suc a1) = F @ a3 : lfnaux F (suc a3) a1 -> nth a2 (lfnaux F a3 (suc a1)) = nth a2 (F @ a3 : lfnaux F (suc a3) a1)
64		lfnauxS	lfnaux F a3 (suc a1) = F @ a3 : lfnaux F (suc a3) a1
65	63, 64	ax_mp	nth a2 (lfnaux F a3 (suc a1)) = nth a2 (F @ a3 : lfnaux F (suc a3) a1)
66		nthZ	nth 0 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ a3)
67		anr	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> a2 = 0
68	67	ntheq1d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = nth 0 (F @ a3 : lfnaux F (suc a3) a1)
69	66, 68	syl6eq	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ a3)
70		add02	a3 + 0 = a3
71	67	addeq2d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> a3 + a2 = a3 + 0
72	70, 71	syl6eq	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> a3 + a2 = a3
73	72	appeq2d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> F @ (a3 + a2) = F @ a3
74	73	suceqd	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> suc (F @ (a3 + a2)) = suc (F @ a3)
75	69, 74	eqtr4d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
76	75	exp	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
77		exsuc	a2 != 0 <-> E. a4 a2 = suc a4
78	77	conv ne	~a2 = 0 <-> E. a4 a2 = suc a4
79		nfal1	F/ a4 A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))
80		nfv	F/ a4 a2 < suc a1
81	79, 80	nfan	F/ a4 A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1
82		nfv	F/ a4 nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
83		anr	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a2 = suc a4
84	83	ntheq1d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = nth (suc a4) (F @ a3 : lfnaux F (suc a3) a1)
85		nthS	nth (suc a4) (F @ a3 : lfnaux F (suc a3) a1) = nth a4 (lfnaux F (suc a3) a1)
86		ltsuc	a4 < a1 <-> suc a4 < suc a1
87	83	lteq1d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> (a2 < suc a1 <-> suc a4 < suc a1)
88		anlr	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a2 < suc a1
89	87, 88	mpbid	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> suc a4 < suc a1
90	86, 89	sylibr	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a4 < a1
91		eal	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) -> A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))
92	91	anwll	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))
93		lfnauxeq2	a5 = suc a3 -> lfnaux F a5 a1 = lfnaux F (suc a3) a1
94	93	ntheq2d	a5 = suc a3 -> nth a4 (lfnaux F a5 a1) = nth a4 (lfnaux F (suc a3) a1)
95		addeq1	a5 = suc a3 -> a5 + a4 = suc a3 + a4
96	95	appeq2d	a5 = suc a3 -> F @ (a5 + a4) = F @ (suc a3 + a4)
97	96	suceqd	a5 = suc a3 -> suc (F @ (a5 + a4)) = suc (F @ (suc a3 + a4))
98	94, 97	eqeqd	a5 = suc a3 -> (nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)) <-> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4)))
99	98	imeq2d	a5 = suc a3 -> (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)) <-> a4 < a1 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4)))
100	99	eale	A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) -> a4 < a1 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4))
101	92, 100	rsyl	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a4 < a1 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4))
102	90, 101	mpd	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4))
103		addSass	suc a3 + a4 = a3 + suc a4
104	83	addeq2d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a3 + a2 = a3 + suc a4
105	103, 104	syl6eqr	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a3 + a2 = suc a3 + a4
106	105	appeq2d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> F @ (a3 + a2) = F @ (suc a3 + a4)
107	106	suceqd	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> suc (F @ (a3 + a2)) = suc (F @ (suc a3 + a4))
108	102, 107	eqtr4d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
109	85, 108	syl5eq	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> nth (suc a4) (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
110	84, 109	eqtrd	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
111	110	exp	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> a2 = suc a4 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
112	81, 82, 111	eexdh	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> E. a4 a2 = suc a4 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
113	78, 112	syl5bi	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> ~a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
114	76, 113	casesd	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
115	65, 114	syl5eq	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2))
116	115	ialda	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) -> A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))
117	116	iald	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) -> A. a2 A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))
118	62, 117	sylbi	A. a2 A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))) -> A. a2 A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))
119	21, 29, 37, 45, 50, 118	ind	A. a2 A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)))
120	13, 119	ax_mp	i < n -> nth i (lfnaux F k n) = suc (F @ (k + i))

1

a2 = i /\ a3 = k -> a2 = i

2

1

lteq1d

a2 = i /\ a3 = k -> (a2 < n <-> i < n)

3

anr

a2 = i /\ a3 = k -> a3 = k

4

3

lfnauxeq2d

a2 = i /\ a3 = k -> lfnaux F a3 n = lfnaux F k n

5

1, 4

ntheqd

a2 = i /\ a3 = k -> nth a2 (lfnaux F a3 n) = nth i (lfnaux F k n)

6

3, 1

addeqd

a2 = i /\ a3 = k -> a3 + a2 = k + i

7

6

appeq2d

a2 = i /\ a3 = k -> F @ (a3 + a2) = F @ (k + i)

8

7

suceqd

a2 = i /\ a3 = k -> suc (F @ (a3 + a2)) = suc (F @ (k + i))

9

5, 8

eqeqd

a2 = i /\ a3 = k -> (nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)) <-> nth i (lfnaux F k n) = suc (F @ (k + i)))

10

2, 9

imeqd

a2 = i /\ a3 = k -> (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)) <-> i < n -> nth i (lfnaux F k n) = suc (F @ (k + i)))

11

10

bi1d

a2 = i /\ a3 = k -> (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))) -> i < n -> nth i (lfnaux F k n) = suc (F @ (k + i))

12

11

ealde

a2 = i -> A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))) -> i < n -> nth i (lfnaux F k n) = suc (F @ (k + i))

13

12

ealie

A. a2 A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))) -> i < n -> nth i (lfnaux F k n) = suc (F @ (k + i))

14

id

_1 = n -> _1 = n

15

14

lteq2d

_1 = n -> (a2 < _1 <-> a2 < n)

16

14

lfnauxeq3d

_1 = n -> lfnaux F a3 _1 = lfnaux F a3 n

17

16

ntheq2d

_1 = n -> nth a2 (lfnaux F a3 _1) = nth a2 (lfnaux F a3 n)

18

17

eqeq1d

_1 = n -> (nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)))

19

15, 18

imeqd

_1 = n -> (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)))

20

19

aleqd

_1 = n -> (A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))))

21

20

aleqd

_1 = n -> (A. a2 A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a2 A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))))

22

id

_1 = 0 -> _1 = 0

23

22

lteq2d

_1 = 0 -> (a2 < _1 <-> a2 < 0)

24

22

lfnauxeq3d

_1 = 0 -> lfnaux F a3 _1 = lfnaux F a3 0

25

24

ntheq2d

_1 = 0 -> nth a2 (lfnaux F a3 _1) = nth a2 (lfnaux F a3 0)

26

25

eqeq1d

_1 = 0 -> (nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2)))

27

23, 26

imeqd

_1 = 0 -> (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2)))

28

27

aleqd

_1 = 0 -> (A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a3 (a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2))))

29

28

aleqd

_1 = 0 -> (A. a2 A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a2 A. a3 (a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2))))

30

id

_1 = a1 -> _1 = a1

31

30

lteq2d

_1 = a1 -> (a2 < _1 <-> a2 < a1)

32

30

lfnauxeq3d

_1 = a1 -> lfnaux F a3 _1 = lfnaux F a3 a1

33

32

ntheq2d

_1 = a1 -> nth a2 (lfnaux F a3 _1) = nth a2 (lfnaux F a3 a1)

34

33

eqeq1d

_1 = a1 -> (nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2)))

35

31, 34

imeqd

_1 = a1 -> (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2)))

36

35

aleqd

_1 = a1 -> (A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))))

37

36

aleqd

_1 = a1 -> (A. a2 A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a2 A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))))

38

id

_1 = suc a1 -> _1 = suc a1

39

38

lteq2d

_1 = suc a1 -> (a2 < _1 <-> a2 < suc a1)

40

38

lfnauxeq3d

_1 = suc a1 -> lfnaux F a3 _1 = lfnaux F a3 (suc a1)

41

40

ntheq2d

_1 = suc a1 -> nth a2 (lfnaux F a3 _1) = nth a2 (lfnaux F a3 (suc a1))

42

41

eqeq1d

_1 = suc a1 -> (nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))

43

39, 42

imeqd

_1 = suc a1 -> (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))

44

43

aleqd

_1 = suc a1 -> (A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2))))

45

44

aleqd

_1 = suc a1 ->
  (A. a2 A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a2 A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2))))

46

absurd

~a2 < 0 -> a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2))

47

lt02

~a2 < 0

48

46, 47

ax_mp

a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2))

49

48

ax_gen

A. a3 (a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2)))

50

49

ax_gen

A. a2 A. a3 (a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2)))

51

anl

a2 = a4 /\ a3 = a5 -> a2 = a4

52

51

lteq1d

a2 = a4 /\ a3 = a5 -> (a2 < a1 <-> a4 < a1)

53

anr

a2 = a4 /\ a3 = a5 -> a3 = a5

54

53

lfnauxeq2d

a2 = a4 /\ a3 = a5 -> lfnaux F a3 a1 = lfnaux F a5 a1

55

51, 54

ntheqd

a2 = a4 /\ a3 = a5 -> nth a2 (lfnaux F a3 a1) = nth a4 (lfnaux F a5 a1)

56

53, 51

addeqd

a2 = a4 /\ a3 = a5 -> a3 + a2 = a5 + a4

57

56

appeq2d

a2 = a4 /\ a3 = a5 -> F @ (a3 + a2) = F @ (a5 + a4)

58

57

suceqd

a2 = a4 /\ a3 = a5 -> suc (F @ (a3 + a2)) = suc (F @ (a5 + a4))

59

55, 58

eqeqd

a2 = a4 /\ a3 = a5 -> (nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2)) <-> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))

60

52, 59

imeqd

a2 = a4 /\ a3 = a5 -> (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2)) <-> a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))

61

60

cbvald

a2 = a4 -> (A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))) <-> A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))))

62

61

cbval

A. a2 A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))) <-> A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))

63

ntheq2

lfnaux F a3 (suc a1) = F @ a3 : lfnaux F (suc a3) a1 -> nth a2 (lfnaux F a3 (suc a1)) = nth a2 (F @ a3 : lfnaux F (suc a3) a1)

64

lfnauxS

lfnaux F a3 (suc a1) = F @ a3 : lfnaux F (suc a3) a1

65

63, 64

ax_mp

nth a2 (lfnaux F a3 (suc a1)) = nth a2 (F @ a3 : lfnaux F (suc a3) a1)

66

nthZ

nth 0 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ a3)

67

anr

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> a2 = 0

68

67

ntheq1d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 ->
  nth a2 (F @ a3 : lfnaux F (suc a3) a1) = nth 0 (F @ a3 : lfnaux F (suc a3) a1)

69

66, 68

syl6eq

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ a3)

70

add02

a3 + 0 = a3

71

67

addeq2d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> a3 + a2 = a3 + 0

72

70, 71

syl6eq

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> a3 + a2 = a3

73

72

appeq2d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> F @ (a3 + a2) = F @ a3

74

73

suceqd

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> suc (F @ (a3 + a2)) = suc (F @ a3)

75

69, 74

eqtr4d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

76

75

exp

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

77

exsuc

a2 != 0 <-> E. a4 a2 = suc a4

79

nfal1

F/ a4 A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))

80

nfv

F/ a4 a2 < suc a1

81

79, 80

nfan

F/ a4 A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1

82

nfv

F/ a4 nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

83

anr

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a2 = suc a4

84

83

ntheq1d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 ->
  nth a2 (F @ a3 : lfnaux F (suc a3) a1) = nth (suc a4) (F @ a3 : lfnaux F (suc a3) a1)

85

nthS

nth (suc a4) (F @ a3 : lfnaux F (suc a3) a1) = nth a4 (lfnaux F (suc a3) a1)

86

ltsuc

a4 < a1 <-> suc a4 < suc a1

87

83

lteq1d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> (a2 < suc a1 <-> suc a4 < suc a1)

88

anlr

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a2 < suc a1

89

87, 88

mpbid

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> suc a4 < suc a1

90

86, 89

sylibr

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a4 < a1

91

eal

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) -> A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))

92

91

anwll

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 ->
  A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))

93

lfnauxeq2

a5 = suc a3 -> lfnaux F a5 a1 = lfnaux F (suc a3) a1

94

93

ntheq2d

a5 = suc a3 -> nth a4 (lfnaux F a5 a1) = nth a4 (lfnaux F (suc a3) a1)

95

addeq1

a5 = suc a3 -> a5 + a4 = suc a3 + a4

96

95

appeq2d

a5 = suc a3 -> F @ (a5 + a4) = F @ (suc a3 + a4)

97

96

suceqd

a5 = suc a3 -> suc (F @ (a5 + a4)) = suc (F @ (suc a3 + a4))

98

94, 97

eqeqd

a5 = suc a3 -> (nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)) <-> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4)))

99

98

imeq2d

a5 = suc a3 -> (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)) <-> a4 < a1 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4)))

100

99

eale

A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) -> a4 < a1 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4))

101

92, 100

rsyl

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 ->
  a4 < a1 ->
  nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4))

102

90, 101

mpd

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4))

103

addSass

suc a3 + a4 = a3 + suc a4

104

83

addeq2d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a3 + a2 = a3 + suc a4

105

103, 104

syl6eqr

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a3 + a2 = suc a3 + a4

106

105

appeq2d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> F @ (a3 + a2) = F @ (suc a3 + a4)

107

106

suceqd

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> suc (F @ (a3 + a2)) = suc (F @ (suc a3 + a4))

108

102, 107

eqtr4d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

109

85, 108

syl5eq

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 ->
  nth (suc a4) (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

110

84, 109

eqtrd

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 ->
  nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

111

110

exp

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 ->
  a2 = suc a4 ->
  nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

112

81, 82, 111

eexdh

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 ->
  E. a4 a2 = suc a4 ->
  nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

113

78, 112

syl5bi

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> ~a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

114

76, 113

casesd

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

115

65, 114

syl5eq

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2))

116

115

ialda

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) -> A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))

117

116

iald

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) -> A. a2 A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))

118

62, 117

sylbi

A. a2 A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))) -> A. a2 A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))

119

21, 29, 37, 45, 50, 118

ind

A. a2 A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)))

120

13, 119

ax_mp

i < n -> nth i (lfnaux F k n) = suc (F @ (k + i))

Theorem lfnauxnth ≪ | index | src | ≫

Axiom use