lfnauxshift - ../examples/peano.mm1

Step	Hyp	Ref	Expression
1		anl	a2 = k1 /\ a3 = k2 -> a2 = k1
2	1	addeq1d	a2 = k1 /\ a3 = k2 -> a2 + i = k1 + i
3	2	appeq2d	a2 = k1 /\ a3 = k2 -> F1 @ (a2 + i) = F1 @ (k1 + i)
4		anr	a2 = k1 /\ a3 = k2 -> a3 = k2
5	4	addeq1d	a2 = k1 /\ a3 = k2 -> a3 + i = k2 + i
6	5	appeq2d	a2 = k1 /\ a3 = k2 -> F2 @ (a3 + i) = F2 @ (k2 + i)
7	3, 6	eqeqd	a2 = k1 /\ a3 = k2 -> (F1 @ (a2 + i) = F2 @ (a3 + i) <-> F1 @ (k1 + i) = F2 @ (k2 + i))
8	7	aleqd	a2 = k1 /\ a3 = k2 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. i F1 @ (k1 + i) = F2 @ (k2 + i))
9	1	lfnauxeq2d	a2 = k1 /\ a3 = k2 -> lfnaux F1 a2 n = lfnaux F1 k1 n
10	4	lfnauxeq2d	a2 = k1 /\ a3 = k2 -> lfnaux F2 a3 n = lfnaux F2 k2 n
11	9, 10	eqeqd	a2 = k1 /\ a3 = k2 -> (lfnaux F1 a2 n = lfnaux F2 a3 n <-> lfnaux F1 k1 n = lfnaux F2 k2 n)
12	8, 11	imeqd	a2 = k1 /\ a3 = k2 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n <-> A. i F1 @ (k1 + i) = F2 @ (k2 + i) -> lfnaux F1 k1 n = lfnaux F2 k2 n)
13	12	bi1d	a2 = k1 /\ a3 = k2 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n) -> A. i F1 @ (k1 + i) = F2 @ (k2 + i) -> lfnaux F1 k1 n = lfnaux F2 k2 n
14	13	ealde	a2 = k1 -> A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n) -> A. i F1 @ (k1 + i) = F2 @ (k2 + i) -> lfnaux F1 k1 n = lfnaux F2 k2 n
15	14	ealie	A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n) -> A. i F1 @ (k1 + i) = F2 @ (k2 + i) -> lfnaux F1 k1 n = lfnaux F2 k2 n
16		biidd	_1 = n -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i))
17		eqsidd	_1 = n -> F1 == F1
18		eqidd	_1 = n -> a2 = a2
19		id	_1 = n -> _1 = n
20	17, 18, 19	lfnauxeqd	_1 = n -> lfnaux F1 a2 _1 = lfnaux F1 a2 n
21		eqsidd	_1 = n -> F2 == F2
22		eqidd	_1 = n -> a3 = a3
23	21, 22, 19	lfnauxeqd	_1 = n -> lfnaux F2 a3 _1 = lfnaux F2 a3 n
24	20, 23	eqeqd	_1 = n -> (lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> lfnaux F1 a2 n = lfnaux F2 a3 n)
25	16, 24	imeqd	_1 = n -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n)
26	25	aleqd	_1 = n -> (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <-> A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n))
27	26	aleqd	_1 = n -> (A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <-> A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n))
28		biidd	_1 = 0 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i))
29		eqsidd	_1 = 0 -> F1 == F1
30		eqidd	_1 = 0 -> a2 = a2
31		id	_1 = 0 -> _1 = 0
32	29, 30, 31	lfnauxeqd	_1 = 0 -> lfnaux F1 a2 _1 = lfnaux F1 a2 0
33		eqsidd	_1 = 0 -> F2 == F2
34		eqidd	_1 = 0 -> a3 = a3
35	33, 34, 31	lfnauxeqd	_1 = 0 -> lfnaux F2 a3 _1 = lfnaux F2 a3 0
36	32, 35	eqeqd	_1 = 0 -> (lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> lfnaux F1 a2 0 = lfnaux F2 a3 0)
37	28, 36	imeqd	_1 = 0 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0)
38	37	aleqd	_1 = 0 -> (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <-> A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0))
39	38	aleqd	_1 = 0 -> (A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <-> A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0))
40		biidd	_1 = a1 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i))
41		eqsidd	_1 = a1 -> F1 == F1
42		eqidd	_1 = a1 -> a2 = a2
43		id	_1 = a1 -> _1 = a1
44	41, 42, 43	lfnauxeqd	_1 = a1 -> lfnaux F1 a2 _1 = lfnaux F1 a2 a1
45		eqsidd	_1 = a1 -> F2 == F2
46		eqidd	_1 = a1 -> a3 = a3
47	45, 46, 43	lfnauxeqd	_1 = a1 -> lfnaux F2 a3 _1 = lfnaux F2 a3 a1
48	44, 47	eqeqd	_1 = a1 -> (lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> lfnaux F1 a2 a1 = lfnaux F2 a3 a1)
49	40, 48	imeqd	_1 = a1 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1)
50	49	aleqd	_1 = a1 -> (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <-> A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1))
51	50	aleqd	_1 = a1 -> (A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <-> A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1))
52		biidd	_1 = suc a1 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i))
53		eqsidd	_1 = suc a1 -> F1 == F1
54		eqidd	_1 = suc a1 -> a2 = a2
55		id	_1 = suc a1 -> _1 = suc a1
56	53, 54, 55	lfnauxeqd	_1 = suc a1 -> lfnaux F1 a2 _1 = lfnaux F1 a2 (suc a1)
57		eqsidd	_1 = suc a1 -> F2 == F2
58		eqidd	_1 = suc a1 -> a3 = a3
59	57, 58, 55	lfnauxeqd	_1 = suc a1 -> lfnaux F2 a3 _1 = lfnaux F2 a3 (suc a1)
60	56, 59	eqeqd	_1 = suc a1 -> (lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))
61	52, 60	imeqd	_1 = suc a1 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))
62	61	aleqd	_1 = suc a1 -> (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <-> A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)))
63	62	aleqd	_1 = suc a1 -> (A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <-> A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)))
64		eqtr4	lfnaux F1 a2 0 = 0 -> lfnaux F2 a3 0 = 0 -> lfnaux F1 a2 0 = lfnaux F2 a3 0
65		lfnaux0	lfnaux F1 a2 0 = 0
66	64, 65	ax_mp	lfnaux F2 a3 0 = 0 -> lfnaux F1 a2 0 = lfnaux F2 a3 0
67		lfnaux0	lfnaux F2 a3 0 = 0
68	66, 67	ax_mp	lfnaux F1 a2 0 = lfnaux F2 a3 0
69	68	a1i	A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0
70	69	ax_gen	A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0)
71	70	ax_gen	A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0)
72		anl	a2 = a4 /\ a3 = a5 -> a2 = a4
73	72	addeq1d	a2 = a4 /\ a3 = a5 -> a2 + i = a4 + i
74	73	appeq2d	a2 = a4 /\ a3 = a5 -> F1 @ (a2 + i) = F1 @ (a4 + i)
75		anr	a2 = a4 /\ a3 = a5 -> a3 = a5
76	75	addeq1d	a2 = a4 /\ a3 = a5 -> a3 + i = a5 + i
77	76	appeq2d	a2 = a4 /\ a3 = a5 -> F2 @ (a3 + i) = F2 @ (a5 + i)
78	74, 77	eqeqd	a2 = a4 /\ a3 = a5 -> (F1 @ (a2 + i) = F2 @ (a3 + i) <-> F1 @ (a4 + i) = F2 @ (a5 + i))
79	78	aleqd	a2 = a4 /\ a3 = a5 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. i F1 @ (a4 + i) = F2 @ (a5 + i))
80	72	lfnauxeq2d	a2 = a4 /\ a3 = a5 -> lfnaux F1 a2 a1 = lfnaux F1 a4 a1
81	75	lfnauxeq2d	a2 = a4 /\ a3 = a5 -> lfnaux F2 a3 a1 = lfnaux F2 a5 a1
82	80, 81	eqeqd	a2 = a4 /\ a3 = a5 -> (lfnaux F1 a2 a1 = lfnaux F2 a3 a1 <-> lfnaux F1 a4 a1 = lfnaux F2 a5 a1)
83	79, 82	imeqd	a2 = a4 /\ a3 = a5 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1 <-> A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1)
84	83	cbvald	a2 = a4 -> (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1) <-> A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1))
85	84	cbval	A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1) <-> A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1)
86		anl	a4 = suc a2 /\ a5 = suc a3 -> a4 = suc a2
87	86	addeq1d	a4 = suc a2 /\ a5 = suc a3 -> a4 + i = suc a2 + i
88	87	appeq2d	a4 = suc a2 /\ a5 = suc a3 -> F1 @ (a4 + i) = F1 @ (suc a2 + i)
89		anr	a4 = suc a2 /\ a5 = suc a3 -> a5 = suc a3
90	89	addeq1d	a4 = suc a2 /\ a5 = suc a3 -> a5 + i = suc a3 + i
91	90	appeq2d	a4 = suc a2 /\ a5 = suc a3 -> F2 @ (a5 + i) = F2 @ (suc a3 + i)
92	88, 91	eqeqd	a4 = suc a2 /\ a5 = suc a3 -> (F1 @ (a4 + i) = F2 @ (a5 + i) <-> F1 @ (suc a2 + i) = F2 @ (suc a3 + i))
93	92	aleqd	a4 = suc a2 /\ a5 = suc a3 -> (A. i F1 @ (a4 + i) = F2 @ (a5 + i) <-> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i))
94	86	lfnauxeq2d	a4 = suc a2 /\ a5 = suc a3 -> lfnaux F1 a4 a1 = lfnaux F1 (suc a2) a1
95	89	lfnauxeq2d	a4 = suc a2 /\ a5 = suc a3 -> lfnaux F2 a5 a1 = lfnaux F2 (suc a3) a1
96	94, 95	eqeqd	a4 = suc a2 /\ a5 = suc a3 -> (lfnaux F1 a4 a1 = lfnaux F2 a5 a1 <-> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1)
97	93, 96	imeqd	a4 = suc a2 /\ a5 = suc a3 -> (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1 <-> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1)
98	97	bi1d	a4 = suc a2 /\ a5 = suc a3 -> (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) -> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1
99	98	ealde	a4 = suc a2 -> A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) -> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1
100	99	ealie	A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) -> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1
101		addeq2	i = a6 -> a2 + i = a2 + a6
102	101	appeq2d	i = a6 -> F1 @ (a2 + i) = F1 @ (a2 + a6)
103		addeq2	i = a6 -> a3 + i = a3 + a6
104	103	appeq2d	i = a6 -> F2 @ (a3 + i) = F2 @ (a3 + a6)
105	102, 104	eqeqd	i = a6 -> (F1 @ (a2 + i) = F2 @ (a3 + i) <-> F1 @ (a2 + a6) = F2 @ (a3 + a6))
106	105	cbval	A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. a6 F1 @ (a2 + a6) = F2 @ (a3 + a6)
107		eqeq	F1 @ (suc a2 + i) = F1 @ (a2 + suc i) -> F2 @ (suc a3 + i) = F2 @ (a3 + suc i) -> (F1 @ (suc a2 + i) = F2 @ (suc a3 + i) <-> F1 @ (a2 + suc i) = F2 @ (a3 + suc i))
108		appeq2	suc a2 + i = a2 + suc i -> F1 @ (suc a2 + i) = F1 @ (a2 + suc i)
109		addSass	suc a2 + i = a2 + suc i
110	108, 109	ax_mp	F1 @ (suc a2 + i) = F1 @ (a2 + suc i)
111	107, 110	ax_mp	F2 @ (suc a3 + i) = F2 @ (a3 + suc i) -> (F1 @ (suc a2 + i) = F2 @ (suc a3 + i) <-> F1 @ (a2 + suc i) = F2 @ (a3 + suc i))
112		appeq2	suc a3 + i = a3 + suc i -> F2 @ (suc a3 + i) = F2 @ (a3 + suc i)
113		addSass	suc a3 + i = a3 + suc i
114	112, 113	ax_mp	F2 @ (suc a3 + i) = F2 @ (a3 + suc i)
115	111, 114	ax_mp	F1 @ (suc a2 + i) = F2 @ (suc a3 + i) <-> F1 @ (a2 + suc i) = F2 @ (a3 + suc i)
116		addeq2	a6 = suc i -> a2 + a6 = a2 + suc i
117	116	appeq2d	a6 = suc i -> F1 @ (a2 + a6) = F1 @ (a2 + suc i)
118		addeq2	a6 = suc i -> a3 + a6 = a3 + suc i
119	118	appeq2d	a6 = suc i -> F2 @ (a3 + a6) = F2 @ (a3 + suc i)
120	117, 119	eqeqd	a6 = suc i -> (F1 @ (a2 + a6) = F2 @ (a3 + a6) <-> F1 @ (a2 + suc i) = F2 @ (a3 + suc i))
121	120	eale	A. a6 F1 @ (a2 + a6) = F2 @ (a3 + a6) -> F1 @ (a2 + suc i) = F2 @ (a3 + suc i)
122	115, 121	sylibr	A. a6 F1 @ (a2 + a6) = F2 @ (a3 + a6) -> F1 @ (suc a2 + i) = F2 @ (suc a3 + i)
123	122	iald	A. a6 F1 @ (a2 + a6) = F2 @ (a3 + a6) -> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i)
124	106, 123	sylbi	A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i)
125	124	imim1i	(A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1) -> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1
126		lfnauxS	lfnaux F1 a2 (suc a1) = F1 @ a2 : lfnaux F1 (suc a2) a1
127		lfnauxS	lfnaux F2 a3 (suc a1) = F2 @ a3 : lfnaux F2 (suc a3) a1
128		add0	a2 + 0 = a2
129		addeq2	i = 0 -> a2 + i = a2 + 0
130	128, 129	syl6eq	i = 0 -> a2 + i = a2
131	130	appeq2d	i = 0 -> F1 @ (a2 + i) = F1 @ a2
132		add0	a3 + 0 = a3
133		addeq2	i = 0 -> a3 + i = a3 + 0
134	132, 133	syl6eq	i = 0 -> a3 + i = a3
135	134	appeq2d	i = 0 -> F2 @ (a3 + i) = F2 @ a3
136	131, 135	eqeqd	i = 0 -> (F1 @ (a2 + i) = F2 @ (a3 + i) <-> F1 @ a2 = F2 @ a3)
137	136	eale	A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> F1 @ a2 = F2 @ a3
138	137	anwl	A. i F1 @ (a2 + i) = F2 @ (a3 + i) /\ lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> F1 @ a2 = F2 @ a3
139		anr	A. i F1 @ (a2 + i) = F2 @ (a3 + i) /\ lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1
140	138, 139	conseqd	A. i F1 @ (a2 + i) = F2 @ (a3 + i) /\ lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> F1 @ a2 : lfnaux F1 (suc a2) a1 = F2 @ a3 : lfnaux F2 (suc a3) a1
141	126, 127, 140	eqtr4g	A. i F1 @ (a2 + i) = F2 @ (a3 + i) /\ lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)
142	141	exp	A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)
143	142	a2i	(A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1) -> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)
144	125, 143	rsyl	(A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1) -> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)
145	100, 144	rsyl	A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) -> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)
146	145	iald	A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) -> A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))
147	146	iald	A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) -> A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))
148	85, 147	sylbi	A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1) -> A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))
149	27, 39, 51, 63, 71, 148	ind	A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n)
150	15, 149	ax_mp	A. i F1 @ (k1 + i) = F2 @ (k2 + i) -> lfnaux F1 k1 n = lfnaux F2 k2 n

1

a2 = k1 /\ a3 = k2 -> a2 = k1

2

1

addeq1d

a2 = k1 /\ a3 = k2 -> a2 + i = k1 + i

3

2

appeq2d

a2 = k1 /\ a3 = k2 -> F1 @ (a2 + i) = F1 @ (k1 + i)

4

anr

a2 = k1 /\ a3 = k2 -> a3 = k2

5

4

addeq1d

a2 = k1 /\ a3 = k2 -> a3 + i = k2 + i

6

5

appeq2d

a2 = k1 /\ a3 = k2 -> F2 @ (a3 + i) = F2 @ (k2 + i)

7

3, 6

eqeqd

a2 = k1 /\ a3 = k2 -> (F1 @ (a2 + i) = F2 @ (a3 + i) <-> F1 @ (k1 + i) = F2 @ (k2 + i))

8

7

aleqd

a2 = k1 /\ a3 = k2 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. i F1 @ (k1 + i) = F2 @ (k2 + i))

9

1

lfnauxeq2d

a2 = k1 /\ a3 = k2 -> lfnaux F1 a2 n = lfnaux F1 k1 n

10

4

lfnauxeq2d

a2 = k1 /\ a3 = k2 -> lfnaux F2 a3 n = lfnaux F2 k2 n

11

9, 10

eqeqd

a2 = k1 /\ a3 = k2 -> (lfnaux F1 a2 n = lfnaux F2 a3 n <-> lfnaux F1 k1 n = lfnaux F2 k2 n)

12

8, 11

imeqd

a2 = k1 /\ a3 = k2 ->
  (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n <-> A. i F1 @ (k1 + i) = F2 @ (k2 + i) -> lfnaux F1 k1 n = lfnaux F2 k2 n)

13

12

bi1d

a2 = k1 /\ a3 = k2 ->
  (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n) ->
  A. i F1 @ (k1 + i) = F2 @ (k2 + i) ->
  lfnaux F1 k1 n = lfnaux F2 k2 n

14

13

ealde

a2 = k1 ->
  A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n) ->
  A. i F1 @ (k1 + i) = F2 @ (k2 + i) ->
  lfnaux F1 k1 n = lfnaux F2 k2 n

15

14

ealie

A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n) -> A. i F1 @ (k1 + i) = F2 @ (k2 + i) -> lfnaux F1 k1 n = lfnaux F2 k2 n

16

biidd

_1 = n -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i))

17

eqsidd

_1 = n -> F1 == F1

18

eqidd

_1 = n -> a2 = a2

19

id

_1 = n -> _1 = n

20

17, 18, 19

lfnauxeqd

_1 = n -> lfnaux F1 a2 _1 = lfnaux F1 a2 n

21

eqsidd

_1 = n -> F2 == F2

22

eqidd

_1 = n -> a3 = a3

23

21, 22, 19

lfnauxeqd

_1 = n -> lfnaux F2 a3 _1 = lfnaux F2 a3 n

24

20, 23

eqeqd

_1 = n -> (lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> lfnaux F1 a2 n = lfnaux F2 a3 n)

25

16, 24

imeqd

_1 = n -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n)

26

25

aleqd

_1 = n ->
  (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <->
    A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n))

27

26

aleqd

_1 = n ->
  (A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <->
    A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n))

28

biidd

_1 = 0 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i))

29

eqsidd

_1 = 0 -> F1 == F1

30

eqidd

_1 = 0 -> a2 = a2

31

id

_1 = 0 -> _1 = 0

32

29, 30, 31

lfnauxeqd

_1 = 0 -> lfnaux F1 a2 _1 = lfnaux F1 a2 0

33

eqsidd

_1 = 0 -> F2 == F2

34

eqidd

_1 = 0 -> a3 = a3

35

33, 34, 31

lfnauxeqd

_1 = 0 -> lfnaux F2 a3 _1 = lfnaux F2 a3 0

36

32, 35

eqeqd

_1 = 0 -> (lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> lfnaux F1 a2 0 = lfnaux F2 a3 0)

37

28, 36

imeqd

_1 = 0 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0)

38

37

aleqd

_1 = 0 ->
  (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <->
    A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0))

39

38

aleqd

_1 = 0 ->
  (A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <->
    A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0))

40

biidd

_1 = a1 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i))

41

eqsidd

_1 = a1 -> F1 == F1

42

eqidd

_1 = a1 -> a2 = a2

43

id

_1 = a1 -> _1 = a1

44

41, 42, 43

lfnauxeqd

_1 = a1 -> lfnaux F1 a2 _1 = lfnaux F1 a2 a1

45

eqsidd

_1 = a1 -> F2 == F2

46

eqidd

_1 = a1 -> a3 = a3

47

45, 46, 43

lfnauxeqd

_1 = a1 -> lfnaux F2 a3 _1 = lfnaux F2 a3 a1

48

44, 47

eqeqd

_1 = a1 -> (lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> lfnaux F1 a2 a1 = lfnaux F2 a3 a1)

49

40, 48

imeqd

_1 = a1 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1)

50

49

aleqd

_1 = a1 ->
  (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <->
    A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1))

51

50

aleqd

_1 = a1 ->
  (A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <->
    A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1))

52

biidd

_1 = suc a1 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i))

53

eqsidd

_1 = suc a1 -> F1 == F1

54

eqidd

_1 = suc a1 -> a2 = a2

55

id

_1 = suc a1 -> _1 = suc a1

56

53, 54, 55

lfnauxeqd

_1 = suc a1 -> lfnaux F1 a2 _1 = lfnaux F1 a2 (suc a1)

57

eqsidd

_1 = suc a1 -> F2 == F2

58

eqidd

_1 = suc a1 -> a3 = a3

59

57, 58, 55

lfnauxeqd

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

60

56, 59

eqeqd

_1 = suc a1 -> (lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))

61

52, 60

imeqd

_1 = suc a1 ->
  (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <->
    A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))

62

61

aleqd

_1 = suc a1 ->
  (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <->
    A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)))

63

62

aleqd

_1 = suc a1 ->
  (A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <->
    A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)))

64

eqtr4

lfnaux F1 a2 0 = 0 -> lfnaux F2 a3 0 = 0 -> lfnaux F1 a2 0 = lfnaux F2 a3 0

65

lfnaux0

lfnaux F1 a2 0 = 0

66

64, 65

ax_mp

lfnaux F2 a3 0 = 0 -> lfnaux F1 a2 0 = lfnaux F2 a3 0

67

lfnaux0

lfnaux F2 a3 0 = 0

68

66, 67

ax_mp

lfnaux F1 a2 0 = lfnaux F2 a3 0

69

68

a1i

A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0

70

69

ax_gen

A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0)

71

70

ax_gen

A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0)

72

anl

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

73

72

addeq1d

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

74

73

appeq2d

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

75

anr

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

76

75

addeq1d

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

77

76

appeq2d

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

78

74, 77

eqeqd

a2 = a4 /\ a3 = a5 -> (F1 @ (a2 + i) = F2 @ (a3 + i) <-> F1 @ (a4 + i) = F2 @ (a5 + i))

79

78

aleqd

a2 = a4 /\ a3 = a5 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. i F1 @ (a4 + i) = F2 @ (a5 + i))

80

72

lfnauxeq2d

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

81

75

lfnauxeq2d

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

82

80, 81

eqeqd

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

83

79, 82

imeqd

a2 = a4 /\ a3 = a5 ->
  (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1 <-> A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1)

84

83

cbvald

a2 = a4 ->
  (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1) <->
    A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1))

85

84

cbval

A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1) <->
  A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1)

86

anl

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

87

86

addeq1d

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

88

87

appeq2d

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

89

anr

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

90

89

addeq1d

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

91

90

appeq2d

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

92

88, 91

eqeqd

a4 = suc a2 /\ a5 = suc a3 -> (F1 @ (a4 + i) = F2 @ (a5 + i) <-> F1 @ (suc a2 + i) = F2 @ (suc a3 + i))

93

92

aleqd

a4 = suc a2 /\ a5 = suc a3 -> (A. i F1 @ (a4 + i) = F2 @ (a5 + i) <-> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i))

94

86

lfnauxeq2d

a4 = suc a2 /\ a5 = suc a3 -> lfnaux F1 a4 a1 = lfnaux F1 (suc a2) a1

95

89

lfnauxeq2d

a4 = suc a2 /\ a5 = suc a3 -> lfnaux F2 a5 a1 = lfnaux F2 (suc a3) a1

96

94, 95

eqeqd

a4 = suc a2 /\ a5 = suc a3 -> (lfnaux F1 a4 a1 = lfnaux F2 a5 a1 <-> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1)

97

93, 96

imeqd

a4 = suc a2 /\ a5 = suc a3 ->
  (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1 <->
    A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1)

98

97

bi1d

a4 = suc a2 /\ a5 = suc a3 ->
  (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) ->
  A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) ->
  lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1

99

98

ealde

a4 = suc a2 ->
  A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) ->
  A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) ->
  lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1

100

99

ealie

A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) ->
  A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) ->
  lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1

101

addeq2

i = a6 -> a2 + i = a2 + a6

102

101

appeq2d

i = a6 -> F1 @ (a2 + i) = F1 @ (a2 + a6)

103

addeq2

i = a6 -> a3 + i = a3 + a6

104

103

appeq2d

i = a6 -> F2 @ (a3 + i) = F2 @ (a3 + a6)

105

102, 104

eqeqd

i = a6 -> (F1 @ (a2 + i) = F2 @ (a3 + i) <-> F1 @ (a2 + a6) = F2 @ (a3 + a6))

106

105

cbval

A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. a6 F1 @ (a2 + a6) = F2 @ (a3 + a6)

107

eqeq

F1 @ (suc a2 + i) = F1 @ (a2 + suc i) ->
  F2 @ (suc a3 + i) = F2 @ (a3 + suc i) ->
  (F1 @ (suc a2 + i) = F2 @ (suc a3 + i) <-> F1 @ (a2 + suc i) = F2 @ (a3 + suc i))

108

appeq2

suc a2 + i = a2 + suc i -> F1 @ (suc a2 + i) = F1 @ (a2 + suc i)

109

addSass

suc a2 + i = a2 + suc i

110

108, 109

ax_mp

F1 @ (suc a2 + i) = F1 @ (a2 + suc i)

111

107, 110

ax_mp

F2 @ (suc a3 + i) = F2 @ (a3 + suc i) -> (F1 @ (suc a2 + i) = F2 @ (suc a3 + i) <-> F1 @ (a2 + suc i) = F2 @ (a3 + suc i))

112

appeq2

suc a3 + i = a3 + suc i -> F2 @ (suc a3 + i) = F2 @ (a3 + suc i)

113

addSass

suc a3 + i = a3 + suc i

114

112, 113

ax_mp

F2 @ (suc a3 + i) = F2 @ (a3 + suc i)

115

111, 114

ax_mp

F1 @ (suc a2 + i) = F2 @ (suc a3 + i) <-> F1 @ (a2 + suc i) = F2 @ (a3 + suc i)

116

addeq2

a6 = suc i -> a2 + a6 = a2 + suc i

117

116

appeq2d

a6 = suc i -> F1 @ (a2 + a6) = F1 @ (a2 + suc i)

118

addeq2

a6 = suc i -> a3 + a6 = a3 + suc i

119

118

appeq2d

a6 = suc i -> F2 @ (a3 + a6) = F2 @ (a3 + suc i)

120

117, 119

eqeqd

a6 = suc i -> (F1 @ (a2 + a6) = F2 @ (a3 + a6) <-> F1 @ (a2 + suc i) = F2 @ (a3 + suc i))

121

120

eale

A. a6 F1 @ (a2 + a6) = F2 @ (a3 + a6) -> F1 @ (a2 + suc i) = F2 @ (a3 + suc i)

122

115, 121

sylibr

A. a6 F1 @ (a2 + a6) = F2 @ (a3 + a6) -> F1 @ (suc a2 + i) = F2 @ (suc a3 + i)

123

122

iald

A. a6 F1 @ (a2 + a6) = F2 @ (a3 + a6) -> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i)

124

106, 123

sylbi

A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i)

125

124

imim1i

(A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1) ->
  A. i F1 @ (a2 + i) = F2 @ (a3 + i) ->
  lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1

126

lfnauxS

lfnaux F1 a2 (suc a1) = F1 @ a2 : lfnaux F1 (suc a2) a1

127

lfnauxS

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

128

add0

a2 + 0 = a2

129

addeq2

i = 0 -> a2 + i = a2 + 0

130

128, 129

syl6eq

i = 0 -> a2 + i = a2

131

130

appeq2d

i = 0 -> F1 @ (a2 + i) = F1 @ a2

132

add0

a3 + 0 = a3

133

addeq2

i = 0 -> a3 + i = a3 + 0

134

132, 133

syl6eq

i = 0 -> a3 + i = a3

135

134

appeq2d

i = 0 -> F2 @ (a3 + i) = F2 @ a3

136

131, 135

eqeqd

i = 0 -> (F1 @ (a2 + i) = F2 @ (a3 + i) <-> F1 @ a2 = F2 @ a3)

137

136

eale

A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> F1 @ a2 = F2 @ a3

138

137

anwl

A. i F1 @ (a2 + i) = F2 @ (a3 + i) /\ lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> F1 @ a2 = F2 @ a3

139

anr

A. i F1 @ (a2 + i) = F2 @ (a3 + i) /\ lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1

140

138, 139

conseqd

A. i F1 @ (a2 + i) = F2 @ (a3 + i) /\ lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> F1 @ a2 : lfnaux F1 (suc a2) a1 = F2 @ a3 : lfnaux F2 (suc a3) a1

141

126, 127, 140

eqtr4g

A. i F1 @ (a2 + i) = F2 @ (a3 + i) /\ lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)

142

141

exp

A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)

143

142

a2i

(A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1) ->
  A. i F1 @ (a2 + i) = F2 @ (a3 + i) ->
  lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)

144

125, 143

rsyl

(A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1) ->
  A. i F1 @ (a2 + i) = F2 @ (a3 + i) ->
  lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)

145

100, 144

rsyl

A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) ->
  A. i F1 @ (a2 + i) = F2 @ (a3 + i) ->
  lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)

146

145

iald

A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) ->
  A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))

147

146

iald

A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) ->
  A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))

148

85, 147

sylbi

A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1) ->
  A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))

149

27, 39, 51, 63, 71, 148

ind

A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n)

150

15, 149

ax_mp

A. i F1 @ (k1 + i) = F2 @ (k2 + i) -> lfnaux F1 k1 n = lfnaux F2 k2 n

Theorem lfnauxshift ≪ | index | src | ≫

Axiom use