seqf1olem1 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > seqf1olem1		Structured version Unicode version

Theorem seqf1olem1 12192

Description: Lemma for seqf1o 12194. (Contributed by Mario Carneiro, 26-Feb-2014.) (Revised by Mario Carneiro, 27-May-2014.)

**Hypotheses**
Ref	Expression
seqf1o.1	$/\$ $/\$
seqf1o.2	$/\$ $/\$
seqf1o.3	$/\$ $/\$ $/\$
seqf1o.4
seqf1o.5
seqf1olem.5
seqf1olem.6
seqf1olem.7
seqf1olem.8

**Assertion**
Ref	Expression
seqf1olem1

Distinct variable groups:

Allowed substitution hint:

(

)

**Proof of Theorem seqf1olem1**
Step	Hyp	Ref	Expression
1		seqf1olem.7	. 2
2		fvex 5861	. . 3
3	2	a1i 11	. 2 $/\$
4		fvex 5861	. . . 4
5		ovex 6308	. . . 4
6	4, 5	ifex 3955	. . 3
7	6	a1i 11	. 2 $/\$
8		iftrue 3893	. . . . . . . . 9
9	8	fveq2d 5855	. . . . . . . 8
10	9	eqeq2d 2418	. . . . . . 7
11	10	adantl 466	. . . . . 6 $/\$ $/\$
12		simprr 760	. . . . . . . . 9 $/\$ $/\$ $/\$
13		elfzelz 11744	. . . . . . . . . . . . 13
14	13	zred 11010	. . . . . . . . . . . 12
15	14	ad2antlr 727	. . . . . . . . . . 11 $/\$ $/\$ $/\$
16		simprl 758	. . . . . . . . . . 11 $/\$ $/\$ $/\$
17	15, 16	gtned 9754	. . . . . . . . . 10 $/\$ $/\$ $/\$
18		seqf1olem.5	. . . . . . . . . . . . . . . . 17
19		f1of 5801	. . . . . . . . . . . . . . . . 17
20	18, 19	syl 17	. . . . . . . . . . . . . . . 16
21	20	ad2antrr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
22		fzssp1 11783	. . . . . . . . . . . . . . . 16
23		simplr 756	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
24	22, 23	sseldi 3442	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
25	21, 24	ffvelrnd 6012	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
26		seqf1o.4	. . . . . . . . . . . . . . . 16
27		elfzp1 11787	. . . . . . . . . . . . . . . 16 $\/$
28	26, 27	syl 17	. . . . . . . . . . . . . . 15 $\/$
29	28	ad2antrr 726	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\/$
30	25, 29	mpbid 212	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$
31	30	ord 377	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
32	18	ad2antrr 726	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
33		f1ocnvfv 6167	. . . . . . . . . . . . . 14 $/\$
34	32, 24, 33	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
35		seqf1olem.8	. . . . . . . . . . . . . 14
36	35	eqeq1i 2411	. . . . . . . . . . . . 13
37	34, 36	syl6ibr 229	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
38	31, 37	syld 44	. . . . . . . . . . 11 $/\$ $/\$ $/\$
39	38	necon1ad 2621	. . . . . . . . . 10 $/\$ $/\$ $/\$
40	17, 39	mpd 15	. . . . . . . . 9 $/\$ $/\$ $/\$
41	12, 40	eqeltrd 2492	. . . . . . . 8 $/\$ $/\$ $/\$
42	12	eqcomd 2412	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
43		f1ocnvfv 6167	. . . . . . . . . . . . 13 $/\$
44	32, 24, 43	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
45	42, 44	mpd 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$
46	45, 16	eqbrtrd 4417	. . . . . . . . . 10 $/\$ $/\$ $/\$
47		iftrue 3893	. . . . . . . . . 10
48	46, 47	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
49	48, 45	eqtr2d 2446	. . . . . . . 8 $/\$ $/\$ $/\$
50	41, 49	jca 532	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
51	50	expr 615	. . . . . 6 $/\$ $/\$ $/\$
52	11, 51	sylbid 217	. . . . 5 $/\$ $/\$ $/\$
53		iffalse 3896	. . . . . . . . 9
54	53	fveq2d 5855	. . . . . . . 8
55	54	eqeq2d 2418	. . . . . . 7
56	55	adantl 466	. . . . . 6 $/\$ $/\$
57		simprr 760	. . . . . . . . 9 $/\$ $/\$ $/\$
58		f1ocnv 5813	. . . . . . . . . . . . . . . . . . 19
59	18, 58	syl 17	. . . . . . . . . . . . . . . . . 18
60		f1of1 5800	. . . . . . . . . . . . . . . . . 18
61	59, 60	syl 17	. . . . . . . . . . . . . . . . 17
62		f1f 5766	. . . . . . . . . . . . . . . . 17
63	61, 62	syl 17	. . . . . . . . . . . . . . . 16
64		peano2uz 11182	. . . . . . . . . . . . . . . . . 18
65	26, 64	syl 17	. . . . . . . . . . . . . . . . 17
66		eluzfz2 11750	. . . . . . . . . . . . . . . . 17
67	65, 66	syl 17	. . . . . . . . . . . . . . . 16
68	63, 67	ffvelrnd 6012	. . . . . . . . . . . . . . 15
69	35, 68	syl5eqel 2496	. . . . . . . . . . . . . 14
70		elfzelz 11744	. . . . . . . . . . . . . 14
71	69, 70	syl 17	. . . . . . . . . . . . 13
72	71	zred 11010	. . . . . . . . . . . 12
73	72	ad2antrr 726	. . . . . . . . . . 11 $/\$ $/\$ $/\$
74	14	ad2antlr 727	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
75		peano2re 9789	. . . . . . . . . . . . 13
76	74, 75	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
77		simprl 758	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
78	73, 74	lenltd 9765	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
79	77, 78	mpbird 234	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
80	74	ltp1d 10518	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
81	73, 74, 76, 79, 80	lelttrd 9776	. . . . . . . . . . 11 $/\$ $/\$ $/\$
82	73, 81	ltned 9755	. . . . . . . . . 10 $/\$ $/\$ $/\$
83	20	ad2antrr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
84		fzp1elp1 11790	. . . . . . . . . . . . . . . 16
85	84	ad2antlr 727	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
86	83, 85	ffvelrnd 6012	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
87		elfzp1 11787	. . . . . . . . . . . . . . . 16 $\/$
88	26, 87	syl 17	. . . . . . . . . . . . . . 15 $\/$
89	88	ad2antrr 726	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\/$
90	86, 89	mpbid 212	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$
91	90	ord 377	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
92	18	ad2antrr 726	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
93		f1ocnvfv 6167	. . . . . . . . . . . . . 14 $/\$
94	92, 85, 93	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
95	35	eqeq1i 2411	. . . . . . . . . . . . 13
96	94, 95	syl6ibr 229	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
97	91, 96	syld 44	. . . . . . . . . . 11 $/\$ $/\$ $/\$
98	97	necon1ad 2621	. . . . . . . . . 10 $/\$ $/\$ $/\$
99	82, 98	mpd 15	. . . . . . . . 9 $/\$ $/\$ $/\$
100	57, 99	eqeltrd 2492	. . . . . . . 8 $/\$ $/\$ $/\$
101	57	eqcomd 2412	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
102		f1ocnvfv 6167	. . . . . . . . . . . . . . 15 $/\$
103	92, 85, 102	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
104	101, 103	mpd 15	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
105	104	breq1d 4407	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
106		lttr 9694	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
107	74, 76, 73, 106	syl3anc 1232	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
108	80, 107	mpand 675	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
109	105, 108	sylbid 217	. . . . . . . . . . 11 $/\$ $/\$ $/\$
110	77, 109	mtod 179	. . . . . . . . . 10 $/\$ $/\$ $/\$
111		iffalse 3896	. . . . . . . . . 10
112	110, 111	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
113	104	oveq1d 6295	. . . . . . . . 9 $/\$ $/\$ $/\$
114	74	recnd 9654	. . . . . . . . . 10 $/\$ $/\$ $/\$
115		ax-1cn 9582	. . . . . . . . . 10
116		pncan 9864	. . . . . . . . . 10 $/\$
117	114, 115, 116	sylancl 662	. . . . . . . . 9 $/\$ $/\$ $/\$
118	112, 113, 117	3eqtrrd 2450	. . . . . . . 8 $/\$ $/\$ $/\$
119	100, 118	jca 532	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
120	119	expr 615	. . . . . 6 $/\$ $/\$ $/\$
121	56, 120	sylbid 217	. . . . 5 $/\$ $/\$ $/\$
122	52, 121	pm2.61dan 794	. . . 4 $/\$ $/\$
123	122	expimpd 603	. . 3 $/\$ $/\$
124	47	eqeq2d 2418	. . . . . . 7
125	124	adantl 466	. . . . . 6 $/\$ $/\$
126		simprr 760	. . . . . . . . . . 11 $/\$ $/\$ $/\$
127	63	ad2antrr 726	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
128		simplr 756	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
129	22, 128	sseldi 3442	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
130	127, 129	ffvelrnd 6012	. . . . . . . . . . 11 $/\$ $/\$ $/\$
131	126, 130	eqeltrd 2492	. . . . . . . . . 10 $/\$ $/\$ $/\$
132		elfzle1 11745	. . . . . . . . . 10
133	131, 132	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
134		elfzelz 11744	. . . . . . . . . . . . 13
135	131, 134	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
136	135	zred 11010	. . . . . . . . . . 11 $/\$ $/\$ $/\$
137	72	ad2antrr 726	. . . . . . . . . . 11 $/\$ $/\$ $/\$
138		eluzelz 11138	. . . . . . . . . . . . . . 15
139	26, 138	syl 17	. . . . . . . . . . . . . 14
140	139	peano2zd 11013	. . . . . . . . . . . . 13
141	140	zred 11010	. . . . . . . . . . . 12
142	141	ad2antrr 726	. . . . . . . . . . 11 $/\$ $/\$ $/\$
143		simprl 758	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
144	126, 143	eqbrtrd 4417	. . . . . . . . . . 11 $/\$ $/\$ $/\$
145		elfzle2 11746	. . . . . . . . . . . . 13
146	69, 145	syl 17	. . . . . . . . . . . 12
147	146	ad2antrr 726	. . . . . . . . . . 11 $/\$ $/\$ $/\$
148	136, 137, 142, 144, 147	ltletrd 9778	. . . . . . . . . 10 $/\$ $/\$ $/\$
149	139	ad2antrr 726	. . . . . . . . . . 11 $/\$ $/\$ $/\$
150		zleltp1 10957	. . . . . . . . . . 11 $/\$
151	135, 149, 150	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$
152	148, 151	mpbird 234	. . . . . . . . 9 $/\$ $/\$ $/\$
153		eluzel2 11134	. . . . . . . . . . . 12
154	26, 153	syl 17	. . . . . . . . . . 11
155	154	ad2antrr 726	. . . . . . . . . 10 $/\$ $/\$ $/\$
156		elfz 11734	. . . . . . . . . 10 $/\$ $/\$ $/\$
157	135, 155, 149, 156	syl3anc 1232	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
158	133, 152, 157	mpbir2and 925	. . . . . . . 8 $/\$ $/\$ $/\$
159	144, 9	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
160	126	fveq2d 5855	. . . . . . . . 9 $/\$ $/\$ $/\$
161	18	ad2antrr 726	. . . . . . . . . 10 $/\$ $/\$ $/\$
162		f1ocnvfv2 6166	. . . . . . . . . 10 $/\$
163	161, 129, 162	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$
164	159, 160, 163	3eqtrrd 2450	. . . . . . . 8 $/\$ $/\$ $/\$
165	158, 164	jca 532	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
166	165	expr 615	. . . . . 6 $/\$ $/\$ $/\$
167	125, 166	sylbid 217	. . . . 5 $/\$ $/\$ $/\$
168	111	eqeq2d 2418	. . . . . . 7
169	168	adantl 466	. . . . . 6 $/\$ $/\$
170	154	zred 11010	. . . . . . . . . . 11
171	170	ad2antrr 726	. . . . . . . . . 10 $/\$ $/\$ $/\$
172	72	ad2antrr 726	. . . . . . . . . 10 $/\$ $/\$ $/\$
173		simprr 760	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
174	63	ad2antrr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
175		simplr 756	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176	22, 175	sseldi 3442	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
177	174, 176	ffvelrnd 6012	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
178		elfzelz 11744	. . . . . . . . . . . . . 14
179	177, 178	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
180		peano2zm 10950	. . . . . . . . . . . . 13
181	179, 180	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
182	173, 181	eqeltrd 2492	. . . . . . . . . . 11 $/\$ $/\$ $/\$
183	182	zred 11010	. . . . . . . . . 10 $/\$ $/\$ $/\$
184		elfzle1 11745	. . . . . . . . . . . 12
185	69, 184	syl 17	. . . . . . . . . . 11
186	185	ad2antrr 726	. . . . . . . . . 10 $/\$ $/\$ $/\$
187		simprl 758	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
188	179	zred 11010	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
189	172, 188	lenltd 9765	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
190	187, 189	mpbird 234	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
191		elfzelz 11744	. . . . . . . . . . . . . . . . . . . 20
192	191	adantl 466	. . . . . . . . . . . . . . . . . . 19 $/\$
193	192	zred 11010	. . . . . . . . . . . . . . . . . 18 $/\$
194	139	zred 11010	. . . . . . . . . . . . . . . . . . . 20
195	194	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
196	141	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$
197		elfzle2 11746	. . . . . . . . . . . . . . . . . . . 20
198	197	adantl 466	. . . . . . . . . . . . . . . . . . 19 $/\$
199	195	ltp1d 10518	. . . . . . . . . . . . . . . . . . 19 $/\$
200	193, 195, 196, 198, 199	lelttrd 9776	. . . . . . . . . . . . . . . . . 18 $/\$
201	193, 200	gtned 9754	. . . . . . . . . . . . . . . . 17 $/\$
202	201	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
203	61	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
204	67	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
205		f1fveq 6153	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
206	203, 204, 176, 205	syl12anc 1230	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
207	206	necon3bid 2663	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
208	202, 207	mpbird 234	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
209	35	neeq1i 2690	. . . . . . . . . . . . . . 15
210	208, 209	sylibr 214	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
211	210	necomd 2676	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
212	172, 188	ltlend 9764	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
213	190, 211, 212	mpbir2and 925	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
214	71	ad2antrr 726	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
215		zltlem1 10959	. . . . . . . . . . . . 13 $/\$
216	214, 179, 215	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
217	213, 216	mpbid 212	. . . . . . . . . . 11 $/\$ $/\$ $/\$
218	217, 173	breqtrrd 4423	. . . . . . . . . 10 $/\$ $/\$ $/\$
219	171, 172, 183, 186, 218	letrd 9775	. . . . . . . . 9 $/\$ $/\$ $/\$
220		elfzle2 11746	. . . . . . . . . . . 12
221	177, 220	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$
222	194	ad2antrr 726	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
223		1re 9627	. . . . . . . . . . . . 13
224		lesubadd 10067	. . . . . . . . . . . . 13 $/\$ $/\$
225	223, 224	mp3an2 1316	. . . . . . . . . . . 12 $/\$
226	188, 222, 225	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
227	221, 226	mpbird 234	. . . . . . . . . 10 $/\$ $/\$ $/\$
228	173, 227	eqbrtrd 4417	. . . . . . . . 9 $/\$ $/\$ $/\$
229	154	ad2antrr 726	. . . . . . . . . 10 $/\$ $/\$ $/\$
230	139	ad2antrr 726	. . . . . . . . . 10 $/\$ $/\$ $/\$
231	182, 229, 230, 156	syl3anc 1232	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
232	219, 228, 231	mpbir2and 925	. . . . . . . 8 $/\$ $/\$ $/\$
233	172, 183	lenltd 9765	. . . . . . . . . . 11 $/\$ $/\$ $/\$
234	218, 233	mpbid 212	. . . . . . . . . 10 $/\$ $/\$ $/\$
235	234, 54	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
236	173	oveq1d 6295	. . . . . . . . . . 11 $/\$ $/\$ $/\$
237	179	zcnd 11011	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
238		npcan 9867	. . . . . . . . . . . 12 $/\$
239	237, 115, 238	sylancl 662	. . . . . . . . . . 11 $/\$ $/\$ $/\$
240	236, 239	eqtrd 2445	. . . . . . . . . 10 $/\$ $/\$ $/\$
241	240	fveq2d 5855	. . . . . . . . 9 $/\$ $/\$ $/\$
242	18	ad2antrr 726	. . . . . . . . . 10 $/\$ $/\$ $/\$
243	242, 176, 162	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$
244	235, 241, 243	3eqtrrd 2450	. . . . . . . 8 $/\$ $/\$ $/\$
245	232, 244	jca 532	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
246	245	expr 615	. . . . . 6 $/\$ $/\$ $/\$
247	169, 246	sylbid 217	. . . . 5 $/\$ $/\$ $/\$
248	167, 247	pm2.61dan 794	. . . 4 $/\$ $/\$
249	248	expimpd 603	. . 3 $/\$ $/\$
250	123, 249	impbid 192	. 2 $/\$ $/\$
251	1, 3, 7, 250	f1od 6508	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 186 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 976

wceq 1407

wcel 1844

wne 2600

cvv 3061

wss 3416

cif 3887 class class class wbr 4397

cmpt 4455

ccnv 4824

wf 5567

wf1 5568

wf1o 5570

cfv 5571 (class class class)co 6280

cc 9522

cr 9523

c1 9525

caddc 9527

clt 9660

cle 9661

cmin 9843

cz 10907

cuz 11129

cfz 11728

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1641 ax-4 1654 ax-5 1727 ax-6 1773 ax-7 1816 ax-8 1846 ax-9 1848 ax-10 1863 ax-11 1868 ax-12 1880 ax-13 2028 ax-ext 2382 ax-sep 4519 ax-nul 4527 ax-pow 4574 ax-pr 4632 ax-un 6576 ax-cnex 9580 ax-resscn 9581 ax-1cn 9582 ax-icn 9583 ax-addcl 9584 ax-addrcl 9585 ax-mulcl 9586 ax-mulrcl 9587 ax-mulcom 9588 ax-addass 9589 ax-mulass 9590 ax-distr 9591 ax-i2m1 9592 ax-1ne0 9593 ax-1rid 9594 ax-rnegex 9595 ax-rrecex 9596 ax-cnre 9597 ax-pre-lttri 9598 ax-pre-lttrn 9599 ax-pre-ltadd 9600 ax-pre-mulgt0 9601

This theorem depends on definitions: df-bi 187 df-or 370 df-an 371 df-3or 977 df-3an 978 df-tru 1410 df-ex 1636 df-nf 1640 df-sb 1766 df-eu 2244 df-mo 2245 df-clab 2390 df-cleq 2396 df-clel 2399 df-nfc 2554 df-ne 2602 df-nel 2603 df-ral 2761 df-rex 2762 df-reu 2763 df-rab 2765 df-v 3063 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3741 df-if 3888 df-pw 3959 df-sn 3975 df-pr 3977 df-tp 3979 df-op 3981 df-uni 4194 df-iun 4275 df-br 4398 df-opab 4456 df-mpt 4457 df-tr 4492 df-eprel 4736 df-id 4740 df-po 4746 df-so 4747 df-fr 4784 df-we 4786 df-xp 4831 df-rel 4832 df-cnv 4833 df-co 4834 df-dm 4835 df-rn 4836 df-res 4837 df-ima 4838 df-pred 5369 df-ord 5415 df-on 5416 df-lim 5417 df-suc 5418 df-iota 5535 df-fun 5573 df-fn 5574 df-f 5575 df-f1 5576 df-fo 5577 df-f1o 5578 df-fv 5579 df-riota 6242 df-ov 6283 df-oprab 6284 df-mpt2 6285 df-om 6686 df-1st 6786 df-2nd 6787 df-wrecs 7015 df-recs 7077 df-rdg 7115 df-er 7350 df-en 7557 df-dom 7558 df-sdom 7559 df-pnf 9662 df-mnf 9663 df-xr 9664 df-ltxr 9665 df-le 9666 df-sub 9845 df-neg 9846 df-nn 10579 df-n0 10839 df-z 10908 df-uz 11130 df-fz 11729

This theorem is referenced by: seqf1olem2 12193

W3C validator