seqf1olem1 - Metamath Proof Explorer

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

Theorem seqf1olem1 12249

Description: Lemma for seqf1o 12251. (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 5873	. . 3
3	2	a1i 11	. 2 $/\$
4		fvex 5873	. . . 4
5		ovex 6316	. . . 4
6	4, 5	ifex 3948	. . 3
7	6	a1i 11	. 2 $/\$
8		iftrue 3886	. . . . . . . . 9
9	8	fveq2d 5867	. . . . . . . 8
10	9	eqeq2d 2460	. . . . . . 7
11	10	adantl 468	. . . . . 6 $/\$ $/\$
12		simprr 765	. . . . . . . . 9 $/\$ $/\$ $/\$
13		elfzelz 11797	. . . . . . . . . . . . 13
14	13	zred 11037	. . . . . . . . . . . 12
15	14	ad2antlr 732	. . . . . . . . . . 11 $/\$ $/\$ $/\$
16		simprl 763	. . . . . . . . . . 11 $/\$ $/\$ $/\$
17	15, 16	gtned 9767	. . . . . . . . . 10 $/\$ $/\$ $/\$
18		seqf1olem.5	. . . . . . . . . . . . . . . . 17
19		f1of 5812	. . . . . . . . . . . . . . . . 17
20	18, 19	syl 17	. . . . . . . . . . . . . . . 16
21	20	ad2antrr 731	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
22		fzssp1 11838	. . . . . . . . . . . . . . . 16
23		simplr 761	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
24	22, 23	sseldi 3429	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
25	21, 24	ffvelrnd 6021	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
26		seqf1o.4	. . . . . . . . . . . . . . . 16
27		elfzp1 11843	. . . . . . . . . . . . . . . 16 $\/$
28	26, 27	syl 17	. . . . . . . . . . . . . . 15 $\/$
29	28	ad2antrr 731	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\/$
30	25, 29	mpbid 214	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$
31	30	ord 379	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
32	18	ad2antrr 731	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
33		f1ocnvfv 6175	. . . . . . . . . . . . . 14 $/\$
34	32, 24, 33	syl2anc 666	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
35		seqf1olem.8	. . . . . . . . . . . . . 14
36	35	eqeq1i 2455	. . . . . . . . . . . . 13
37	34, 36	syl6ibr 231	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
38	31, 37	syld 45	. . . . . . . . . . 11 $/\$ $/\$ $/\$
39	38	necon1ad 2640	. . . . . . . . . 10 $/\$ $/\$ $/\$
40	17, 39	mpd 15	. . . . . . . . 9 $/\$ $/\$ $/\$
41	12, 40	eqeltrd 2528	. . . . . . . 8 $/\$ $/\$ $/\$
42	12	eqcomd 2456	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
43		f1ocnvfv 6175	. . . . . . . . . . . . 13 $/\$
44	32, 24, 43	syl2anc 666	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
45	42, 44	mpd 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$
46	45, 16	eqbrtrd 4422	. . . . . . . . . 10 $/\$ $/\$ $/\$
47		iftrue 3886	. . . . . . . . . 10
48	46, 47	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
49	48, 45	eqtr2d 2485	. . . . . . . 8 $/\$ $/\$ $/\$
50	41, 49	jca 535	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
51	50	expr 619	. . . . . 6 $/\$ $/\$ $/\$
52	11, 51	sylbid 219	. . . . 5 $/\$ $/\$ $/\$
53		iffalse 3889	. . . . . . . . 9
54	53	fveq2d 5867	. . . . . . . 8
55	54	eqeq2d 2460	. . . . . . 7
56	55	adantl 468	. . . . . 6 $/\$ $/\$
57		simprr 765	. . . . . . . . 9 $/\$ $/\$ $/\$
58		f1ocnv 5824	. . . . . . . . . . . . . . . . . . 19
59	18, 58	syl 17	. . . . . . . . . . . . . . . . . 18
60		f1of1 5811	. . . . . . . . . . . . . . . . . 18
61	59, 60	syl 17	. . . . . . . . . . . . . . . . 17
62		f1f 5777	. . . . . . . . . . . . . . . . 17
63	61, 62	syl 17	. . . . . . . . . . . . . . . 16
64		peano2uz 11209	. . . . . . . . . . . . . . . . . 18
65	26, 64	syl 17	. . . . . . . . . . . . . . . . 17
66		eluzfz2 11804	. . . . . . . . . . . . . . . . 17
67	65, 66	syl 17	. . . . . . . . . . . . . . . 16
68	63, 67	ffvelrnd 6021	. . . . . . . . . . . . . . 15
69	35, 68	syl5eqel 2532	. . . . . . . . . . . . . 14
70		elfzelz 11797	. . . . . . . . . . . . . 14
71	69, 70	syl 17	. . . . . . . . . . . . 13
72	71	zred 11037	. . . . . . . . . . . 12
73	72	ad2antrr 731	. . . . . . . . . . 11 $/\$ $/\$ $/\$
74	14	ad2antlr 732	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
75		peano2re 9803	. . . . . . . . . . . . 13
76	74, 75	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
77		simprl 763	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
78	73, 74	lenltd 9778	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
79	77, 78	mpbird 236	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
80	74	ltp1d 10534	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
81	73, 74, 76, 79, 80	lelttrd 9790	. . . . . . . . . . 11 $/\$ $/\$ $/\$
82	73, 81	ltned 9768	. . . . . . . . . 10 $/\$ $/\$ $/\$
83	20	ad2antrr 731	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
84		fzp1elp1 11846	. . . . . . . . . . . . . . . 16
85	84	ad2antlr 732	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
86	83, 85	ffvelrnd 6021	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
87		elfzp1 11843	. . . . . . . . . . . . . . . 16 $\/$
88	26, 87	syl 17	. . . . . . . . . . . . . . 15 $\/$
89	88	ad2antrr 731	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\/$
90	86, 89	mpbid 214	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$
91	90	ord 379	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
92	18	ad2antrr 731	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
93		f1ocnvfv 6175	. . . . . . . . . . . . . 14 $/\$
94	92, 85, 93	syl2anc 666	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
95	35	eqeq1i 2455	. . . . . . . . . . . . 13
96	94, 95	syl6ibr 231	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
97	91, 96	syld 45	. . . . . . . . . . 11 $/\$ $/\$ $/\$
98	97	necon1ad 2640	. . . . . . . . . 10 $/\$ $/\$ $/\$
99	82, 98	mpd 15	. . . . . . . . 9 $/\$ $/\$ $/\$
100	57, 99	eqeltrd 2528	. . . . . . . 8 $/\$ $/\$ $/\$
101	57	eqcomd 2456	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
102		f1ocnvfv 6175	. . . . . . . . . . . . . . 15 $/\$
103	92, 85, 102	syl2anc 666	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
104	101, 103	mpd 15	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
105	104	breq1d 4411	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
106		lttr 9707	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
107	74, 76, 73, 106	syl3anc 1267	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
108	80, 107	mpand 680	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
109	105, 108	sylbid 219	. . . . . . . . . . 11 $/\$ $/\$ $/\$
110	77, 109	mtod 181	. . . . . . . . . 10 $/\$ $/\$ $/\$
111		iffalse 3889	. . . . . . . . . 10
112	110, 111	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
113	104	oveq1d 6303	. . . . . . . . 9 $/\$ $/\$ $/\$
114	74	recnd 9666	. . . . . . . . . 10 $/\$ $/\$ $/\$
115		ax-1cn 9594	. . . . . . . . . 10
116		pncan 9878	. . . . . . . . . 10 $/\$
117	114, 115, 116	sylancl 667	. . . . . . . . 9 $/\$ $/\$ $/\$
118	112, 113, 117	3eqtrrd 2489	. . . . . . . 8 $/\$ $/\$ $/\$
119	100, 118	jca 535	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
120	119	expr 619	. . . . . 6 $/\$ $/\$ $/\$
121	56, 120	sylbid 219	. . . . 5 $/\$ $/\$ $/\$
122	52, 121	pm2.61dan 799	. . . 4 $/\$ $/\$
123	122	expimpd 607	. . 3 $/\$ $/\$
124	47	eqeq2d 2460	. . . . . . 7
125	124	adantl 468	. . . . . 6 $/\$ $/\$
126		simprr 765	. . . . . . . . . . 11 $/\$ $/\$ $/\$
127	63	ad2antrr 731	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
128		simplr 761	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
129	22, 128	sseldi 3429	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
130	127, 129	ffvelrnd 6021	. . . . . . . . . . 11 $/\$ $/\$ $/\$
131	126, 130	eqeltrd 2528	. . . . . . . . . 10 $/\$ $/\$ $/\$
132		elfzle1 11799	. . . . . . . . . 10
133	131, 132	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
134		elfzelz 11797	. . . . . . . . . . . . 13
135	131, 134	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
136	135	zred 11037	. . . . . . . . . . 11 $/\$ $/\$ $/\$
137	72	ad2antrr 731	. . . . . . . . . . 11 $/\$ $/\$ $/\$
138		eluzelz 11165	. . . . . . . . . . . . . . 15
139	26, 138	syl 17	. . . . . . . . . . . . . 14
140	139	peano2zd 11040	. . . . . . . . . . . . 13
141	140	zred 11037	. . . . . . . . . . . 12
142	141	ad2antrr 731	. . . . . . . . . . 11 $/\$ $/\$ $/\$
143		simprl 763	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
144	126, 143	eqbrtrd 4422	. . . . . . . . . . 11 $/\$ $/\$ $/\$
145		elfzle2 11800	. . . . . . . . . . . . 13
146	69, 145	syl 17	. . . . . . . . . . . 12
147	146	ad2antrr 731	. . . . . . . . . . 11 $/\$ $/\$ $/\$
148	136, 137, 142, 144, 147	ltletrd 9792	. . . . . . . . . 10 $/\$ $/\$ $/\$
149	139	ad2antrr 731	. . . . . . . . . . 11 $/\$ $/\$ $/\$
150		zleltp1 10984	. . . . . . . . . . 11 $/\$
151	135, 149, 150	syl2anc 666	. . . . . . . . . 10 $/\$ $/\$ $/\$
152	148, 151	mpbird 236	. . . . . . . . 9 $/\$ $/\$ $/\$
153		eluzel2 11161	. . . . . . . . . . . 12
154	26, 153	syl 17	. . . . . . . . . . 11
155	154	ad2antrr 731	. . . . . . . . . 10 $/\$ $/\$ $/\$
156		elfz 11787	. . . . . . . . . 10 $/\$ $/\$ $/\$
157	135, 155, 149, 156	syl3anc 1267	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
158	133, 152, 157	mpbir2and 932	. . . . . . . 8 $/\$ $/\$ $/\$
159	144, 9	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
160	126	fveq2d 5867	. . . . . . . . 9 $/\$ $/\$ $/\$
161	18	ad2antrr 731	. . . . . . . . . 10 $/\$ $/\$ $/\$
162		f1ocnvfv2 6174	. . . . . . . . . 10 $/\$
163	161, 129, 162	syl2anc 666	. . . . . . . . 9 $/\$ $/\$ $/\$
164	159, 160, 163	3eqtrrd 2489	. . . . . . . 8 $/\$ $/\$ $/\$
165	158, 164	jca 535	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
166	165	expr 619	. . . . . 6 $/\$ $/\$ $/\$
167	125, 166	sylbid 219	. . . . 5 $/\$ $/\$ $/\$
168	111	eqeq2d 2460	. . . . . . 7
169	168	adantl 468	. . . . . 6 $/\$ $/\$
170	154	zred 11037	. . . . . . . . . . 11
171	170	ad2antrr 731	. . . . . . . . . 10 $/\$ $/\$ $/\$
172	72	ad2antrr 731	. . . . . . . . . 10 $/\$ $/\$ $/\$
173		simprr 765	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
174	63	ad2antrr 731	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
175		simplr 761	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176	22, 175	sseldi 3429	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
177	174, 176	ffvelrnd 6021	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
178		elfzelz 11797	. . . . . . . . . . . . . 14
179	177, 178	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
180		peano2zm 10977	. . . . . . . . . . . . 13
181	179, 180	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
182	173, 181	eqeltrd 2528	. . . . . . . . . . 11 $/\$ $/\$ $/\$
183	182	zred 11037	. . . . . . . . . 10 $/\$ $/\$ $/\$
184		elfzle1 11799	. . . . . . . . . . . 12
185	69, 184	syl 17	. . . . . . . . . . 11
186	185	ad2antrr 731	. . . . . . . . . 10 $/\$ $/\$ $/\$
187		simprl 763	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
188	179	zred 11037	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
189	172, 188	lenltd 9778	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
190	187, 189	mpbird 236	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
191		elfzelz 11797	. . . . . . . . . . . . . . . . . . . 20
192	191	adantl 468	. . . . . . . . . . . . . . . . . . 19 $/\$
193	192	zred 11037	. . . . . . . . . . . . . . . . . 18 $/\$
194	139	zred 11037	. . . . . . . . . . . . . . . . . . . 20
195	194	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$
196	141	adantr 467	. . . . . . . . . . . . . . . . . . 19 $/\$
197		elfzle2 11800	. . . . . . . . . . . . . . . . . . . 20
198	197	adantl 468	. . . . . . . . . . . . . . . . . . 19 $/\$
199	195	ltp1d 10534	. . . . . . . . . . . . . . . . . . 19 $/\$
200	193, 195, 196, 198, 199	lelttrd 9790	. . . . . . . . . . . . . . . . . 18 $/\$
201	193, 200	gtned 9767	. . . . . . . . . . . . . . . . 17 $/\$
202	201	adantr 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
203	61	ad2antrr 731	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
204	67	ad2antrr 731	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
205		f1fveq 6161	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
206	203, 204, 176, 205	syl12anc 1265	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
207	206	necon3bid 2667	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
208	202, 207	mpbird 236	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
209	35	neeq1i 2687	. . . . . . . . . . . . . . 15
210	208, 209	sylibr 216	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
211	210	necomd 2678	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
212	172, 188	ltlend 9777	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
213	190, 211, 212	mpbir2and 932	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
214	71	ad2antrr 731	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
215		zltlem1 10986	. . . . . . . . . . . . 13 $/\$
216	214, 179, 215	syl2anc 666	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
217	213, 216	mpbid 214	. . . . . . . . . . 11 $/\$ $/\$ $/\$
218	217, 173	breqtrrd 4428	. . . . . . . . . 10 $/\$ $/\$ $/\$
219	171, 172, 183, 186, 218	letrd 9789	. . . . . . . . 9 $/\$ $/\$ $/\$
220		elfzle2 11800	. . . . . . . . . . . 12
221	177, 220	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$
222	194	ad2antrr 731	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
223		1re 9639	. . . . . . . . . . . . 13
224		lesubadd 10083	. . . . . . . . . . . . 13 $/\$ $/\$
225	223, 224	mp3an2 1351	. . . . . . . . . . . 12 $/\$
226	188, 222, 225	syl2anc 666	. . . . . . . . . . 11 $/\$ $/\$ $/\$
227	221, 226	mpbird 236	. . . . . . . . . 10 $/\$ $/\$ $/\$
228	173, 227	eqbrtrd 4422	. . . . . . . . 9 $/\$ $/\$ $/\$
229	154	ad2antrr 731	. . . . . . . . . 10 $/\$ $/\$ $/\$
230	139	ad2antrr 731	. . . . . . . . . 10 $/\$ $/\$ $/\$
231	182, 229, 230, 156	syl3anc 1267	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
232	219, 228, 231	mpbir2and 932	. . . . . . . 8 $/\$ $/\$ $/\$
233	172, 183	lenltd 9778	. . . . . . . . . . 11 $/\$ $/\$ $/\$
234	218, 233	mpbid 214	. . . . . . . . . 10 $/\$ $/\$ $/\$
235	234, 54	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
236	173	oveq1d 6303	. . . . . . . . . . 11 $/\$ $/\$ $/\$
237	179	zcnd 11038	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
238		npcan 9881	. . . . . . . . . . . 12 $/\$
239	237, 115, 238	sylancl 667	. . . . . . . . . . 11 $/\$ $/\$ $/\$
240	236, 239	eqtrd 2484	. . . . . . . . . 10 $/\$ $/\$ $/\$
241	240	fveq2d 5867	. . . . . . . . 9 $/\$ $/\$ $/\$
242	18	ad2antrr 731	. . . . . . . . . 10 $/\$ $/\$ $/\$
243	242, 176, 162	syl2anc 666	. . . . . . . . 9 $/\$ $/\$ $/\$
244	235, 241, 243	3eqtrrd 2489	. . . . . . . 8 $/\$ $/\$ $/\$
245	232, 244	jca 535	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
246	245	expr 619	. . . . . 6 $/\$ $/\$ $/\$
247	169, 246	sylbid 219	. . . . 5 $/\$ $/\$ $/\$
248	167, 247	pm2.61dan 799	. . . 4 $/\$ $/\$
249	248	expimpd 607	. . 3 $/\$ $/\$
250	123, 249	impbid 194	. 2 $/\$ $/\$
251	1, 3, 7, 250	f1od 6516	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $/\$ w3a 984

wceq 1443

wcel 1886

wne 2621

cvv 3044

wss 3403

cif 3880 class class class wbr 4401

cmpt 4460

ccnv 4832

wf 5577

wf1 5578

wf1o 5580

cfv 5581 (class class class)co 6288

cc 9534

cr 9535

c1 9537

caddc 9539

clt 9672

cle 9673

cmin 9857

cz 10934

cuz 11156

cfz 11781

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-er 7360 df-en 7567 df-dom 7568 df-sdom 7569 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-nn 10607 df-n0 10867 df-z 10935 df-uz 11157 df-fz 11782

This theorem is referenced by: seqf1olem2 12250

W3C validator