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 12840

Description: Lemma for seqf1o 12842. (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		fvexd 6203	. 2 $/\$
3		fvex 6201	. . . 4
4		ovex 6678	. . . 4
5	3, 4	ifex 4156	. . 3
6	5	a1i 11	. 2 $/\$
7		iftrue 4092	. . . . . . . . 9
8	7	fveq2d 6195	. . . . . . . 8
9	8	eqeq2d 2632	. . . . . . 7
10	9	adantl 482	. . . . . 6 $/\$ $/\$
11		simprr 796	. . . . . . . . 9 $/\$ $/\$ $/\$
12		elfzelz 12342	. . . . . . . . . . . . 13
13	12	zred 11482	. . . . . . . . . . . 12
14	13	ad2antlr 763	. . . . . . . . . . 11 $/\$ $/\$ $/\$
15		simprl 794	. . . . . . . . . . 11 $/\$ $/\$ $/\$
16	14, 15	gtned 10172	. . . . . . . . . 10 $/\$ $/\$ $/\$
17		seqf1olem.5	. . . . . . . . . . . . . . . . 17
18		f1of 6137	. . . . . . . . . . . . . . . . 17
19	17, 18	syl 17	. . . . . . . . . . . . . . . 16
20	19	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
21		fzssp1 12384	. . . . . . . . . . . . . . . 16
22		simplr 792	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
23	21, 22	sseldi 3601	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
24	20, 23	ffvelrnd 6360	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
25		seqf1o.4	. . . . . . . . . . . . . . . 16
26		elfzp1 12391	. . . . . . . . . . . . . . . 16 $\/$
27	25, 26	syl 17	. . . . . . . . . . . . . . 15 $\/$
28	27	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\/$
29	24, 28	mpbid 222	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$
30	29	ord 392	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
31	17	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
32		f1ocnvfv 6534	. . . . . . . . . . . . . 14 $/\$
33	31, 23, 32	syl2anc 693	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
34		seqf1olem.8	. . . . . . . . . . . . . 14
35	34	eqeq1i 2627	. . . . . . . . . . . . 13
36	33, 35	syl6ibr 242	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
37	30, 36	syld 47	. . . . . . . . . . 11 $/\$ $/\$ $/\$
38	37	necon1ad 2811	. . . . . . . . . 10 $/\$ $/\$ $/\$
39	16, 38	mpd 15	. . . . . . . . 9 $/\$ $/\$ $/\$
40	11, 39	eqeltrd 2701	. . . . . . . 8 $/\$ $/\$ $/\$
41	11	eqcomd 2628	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
42		f1ocnvfv 6534	. . . . . . . . . . . . 13 $/\$
43	31, 23, 42	syl2anc 693	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
44	41, 43	mpd 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$
45	44, 15	eqbrtrd 4675	. . . . . . . . . 10 $/\$ $/\$ $/\$
46		iftrue 4092	. . . . . . . . . 10
47	45, 46	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
48	47, 44	eqtr2d 2657	. . . . . . . 8 $/\$ $/\$ $/\$
49	40, 48	jca 554	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
50	49	expr 643	. . . . . 6 $/\$ $/\$ $/\$
51	10, 50	sylbid 230	. . . . 5 $/\$ $/\$ $/\$
52		iffalse 4095	. . . . . . . . 9
53	52	fveq2d 6195	. . . . . . . 8
54	53	eqeq2d 2632	. . . . . . 7
55	54	adantl 482	. . . . . 6 $/\$ $/\$
56		simprr 796	. . . . . . . . 9 $/\$ $/\$ $/\$
57		f1ocnv 6149	. . . . . . . . . . . . . . . . . . 19
58	17, 57	syl 17	. . . . . . . . . . . . . . . . . 18
59		f1of1 6136	. . . . . . . . . . . . . . . . . 18
60	58, 59	syl 17	. . . . . . . . . . . . . . . . 17
61		f1f 6101	. . . . . . . . . . . . . . . . 17
62	60, 61	syl 17	. . . . . . . . . . . . . . . 16
63		peano2uz 11741	. . . . . . . . . . . . . . . . . 18
64	25, 63	syl 17	. . . . . . . . . . . . . . . . 17
65		eluzfz2 12349	. . . . . . . . . . . . . . . . 17
66	64, 65	syl 17	. . . . . . . . . . . . . . . 16
67	62, 66	ffvelrnd 6360	. . . . . . . . . . . . . . 15
68	34, 67	syl5eqel 2705	. . . . . . . . . . . . . 14
69		elfzelz 12342	. . . . . . . . . . . . . 14
70	68, 69	syl 17	. . . . . . . . . . . . 13
71	70	zred 11482	. . . . . . . . . . . 12
72	71	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$
73	13	ad2antlr 763	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
74		peano2re 10209	. . . . . . . . . . . . 13
75	73, 74	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
76		simprl 794	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
77	72, 73	lenltd 10183	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
78	76, 77	mpbird 247	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
79	73	ltp1d 10954	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
80	72, 73, 75, 78, 79	lelttrd 10195	. . . . . . . . . . 11 $/\$ $/\$ $/\$
81	72, 80	ltned 10173	. . . . . . . . . 10 $/\$ $/\$ $/\$
82	19	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
83		fzp1elp1 12394	. . . . . . . . . . . . . . . 16
84	83	ad2antlr 763	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
85	82, 84	ffvelrnd 6360	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
86		elfzp1 12391	. . . . . . . . . . . . . . . 16 $\/$
87	25, 86	syl 17	. . . . . . . . . . . . . . 15 $\/$
88	87	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\/$
89	85, 88	mpbid 222	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$
90	89	ord 392	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
91	17	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
92		f1ocnvfv 6534	. . . . . . . . . . . . . 14 $/\$
93	91, 84, 92	syl2anc 693	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
94	34	eqeq1i 2627	. . . . . . . . . . . . 13
95	93, 94	syl6ibr 242	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
96	90, 95	syld 47	. . . . . . . . . . 11 $/\$ $/\$ $/\$
97	96	necon1ad 2811	. . . . . . . . . 10 $/\$ $/\$ $/\$
98	81, 97	mpd 15	. . . . . . . . 9 $/\$ $/\$ $/\$
99	56, 98	eqeltrd 2701	. . . . . . . 8 $/\$ $/\$ $/\$
100	56	eqcomd 2628	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
101		f1ocnvfv 6534	. . . . . . . . . . . . . . 15 $/\$
102	91, 84, 101	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
103	100, 102	mpd 15	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
104	103	breq1d 4663	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
105		lttr 10114	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
106	73, 75, 72, 105	syl3anc 1326	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
107	79, 106	mpand 711	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
108	104, 107	sylbid 230	. . . . . . . . . . 11 $/\$ $/\$ $/\$
109	76, 108	mtod 189	. . . . . . . . . 10 $/\$ $/\$ $/\$
110		iffalse 4095	. . . . . . . . . 10
111	109, 110	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
112	103	oveq1d 6665	. . . . . . . . 9 $/\$ $/\$ $/\$
113	73	recnd 10068	. . . . . . . . . 10 $/\$ $/\$ $/\$
114		ax-1cn 9994	. . . . . . . . . 10
115		pncan 10287	. . . . . . . . . 10 $/\$
116	113, 114, 115	sylancl 694	. . . . . . . . 9 $/\$ $/\$ $/\$
117	111, 112, 116	3eqtrrd 2661	. . . . . . . 8 $/\$ $/\$ $/\$
118	99, 117	jca 554	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
119	118	expr 643	. . . . . 6 $/\$ $/\$ $/\$
120	55, 119	sylbid 230	. . . . 5 $/\$ $/\$ $/\$
121	51, 120	pm2.61dan 832	. . . 4 $/\$ $/\$
122	121	expimpd 629	. . 3 $/\$ $/\$
123	46	eqeq2d 2632	. . . . . . 7
124	123	adantl 482	. . . . . 6 $/\$ $/\$
125		simprr 796	. . . . . . . . . . 11 $/\$ $/\$ $/\$
126	62	ad2antrr 762	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
127		simplr 792	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
128	21, 127	sseldi 3601	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
129	126, 128	ffvelrnd 6360	. . . . . . . . . . 11 $/\$ $/\$ $/\$
130	125, 129	eqeltrd 2701	. . . . . . . . . 10 $/\$ $/\$ $/\$
131		elfzle1 12344	. . . . . . . . . 10
132	130, 131	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
133		elfzelz 12342	. . . . . . . . . . . . 13
134	130, 133	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
135	134	zred 11482	. . . . . . . . . . 11 $/\$ $/\$ $/\$
136	71	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$
137		eluzelz 11697	. . . . . . . . . . . . . . 15
138	25, 137	syl 17	. . . . . . . . . . . . . 14
139	138	peano2zd 11485	. . . . . . . . . . . . 13
140	139	zred 11482	. . . . . . . . . . . 12
141	140	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$
142		simprl 794	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
143	125, 142	eqbrtrd 4675	. . . . . . . . . . 11 $/\$ $/\$ $/\$
144		elfzle2 12345	. . . . . . . . . . . . 13
145	68, 144	syl 17	. . . . . . . . . . . 12
146	145	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$
147	135, 136, 141, 143, 146	ltletrd 10197	. . . . . . . . . 10 $/\$ $/\$ $/\$
148	138	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$
149		zleltp1 11428	. . . . . . . . . . 11 $/\$
150	134, 148, 149	syl2anc 693	. . . . . . . . . 10 $/\$ $/\$ $/\$
151	147, 150	mpbird 247	. . . . . . . . 9 $/\$ $/\$ $/\$
152		eluzel2 11692	. . . . . . . . . . . 12
153	25, 152	syl 17	. . . . . . . . . . 11
154	153	ad2antrr 762	. . . . . . . . . 10 $/\$ $/\$ $/\$
155		elfz 12332	. . . . . . . . . 10 $/\$ $/\$ $/\$
156	134, 154, 148, 155	syl3anc 1326	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
157	132, 151, 156	mpbir2and 957	. . . . . . . 8 $/\$ $/\$ $/\$
158	143, 8	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
159	125	fveq2d 6195	. . . . . . . . 9 $/\$ $/\$ $/\$
160	17	ad2antrr 762	. . . . . . . . . 10 $/\$ $/\$ $/\$
161		f1ocnvfv2 6533	. . . . . . . . . 10 $/\$
162	160, 128, 161	syl2anc 693	. . . . . . . . 9 $/\$ $/\$ $/\$
163	158, 159, 162	3eqtrrd 2661	. . . . . . . 8 $/\$ $/\$ $/\$
164	157, 163	jca 554	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
165	164	expr 643	. . . . . 6 $/\$ $/\$ $/\$
166	124, 165	sylbid 230	. . . . 5 $/\$ $/\$ $/\$
167	110	eqeq2d 2632	. . . . . . 7
168	167	adantl 482	. . . . . 6 $/\$ $/\$
169	153	zred 11482	. . . . . . . . . . 11
170	169	ad2antrr 762	. . . . . . . . . 10 $/\$ $/\$ $/\$
171	71	ad2antrr 762	. . . . . . . . . 10 $/\$ $/\$ $/\$
172		simprr 796	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
173	62	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
174		simplr 792	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
175	21, 174	sseldi 3601	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
176	173, 175	ffvelrnd 6360	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
177		elfzelz 12342	. . . . . . . . . . . . . 14
178	176, 177	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
179		peano2zm 11420	. . . . . . . . . . . . 13
180	178, 179	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
181	172, 180	eqeltrd 2701	. . . . . . . . . . 11 $/\$ $/\$ $/\$
182	181	zred 11482	. . . . . . . . . 10 $/\$ $/\$ $/\$
183		elfzle1 12344	. . . . . . . . . . . 12
184	68, 183	syl 17	. . . . . . . . . . 11
185	184	ad2antrr 762	. . . . . . . . . 10 $/\$ $/\$ $/\$
186		simprl 794	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
187	178	zred 11482	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
188	171, 187	lenltd 10183	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
189	186, 188	mpbird 247	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
190		elfzelz 12342	. . . . . . . . . . . . . . . . . . . 20
191	190	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
192	191	zred 11482	. . . . . . . . . . . . . . . . . 18 $/\$
193	138	zred 11482	. . . . . . . . . . . . . . . . . . . 20
194	193	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
195	140	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
196		elfzle2 12345	. . . . . . . . . . . . . . . . . . . 20
197	196	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
198	194	ltp1d 10954	. . . . . . . . . . . . . . . . . . 19 $/\$
199	192, 194, 195, 197, 198	lelttrd 10195	. . . . . . . . . . . . . . . . . 18 $/\$
200	192, 199	gtned 10172	. . . . . . . . . . . . . . . . 17 $/\$
201	200	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
202	60	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
203	66	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
204		f1fveq 6519	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
205	202, 203, 175, 204	syl12anc 1324	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
206	205	necon3bid 2838	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
207	201, 206	mpbird 247	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
208	34	neeq1i 2858	. . . . . . . . . . . . . . 15
209	207, 208	sylibr 224	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
210	209	necomd 2849	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
211	171, 187	ltlend 10182	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
212	189, 210, 211	mpbir2and 957	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
213	70	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
214		zltlem1 11430	. . . . . . . . . . . . 13 $/\$
215	213, 178, 214	syl2anc 693	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
216	212, 215	mpbid 222	. . . . . . . . . . 11 $/\$ $/\$ $/\$
217	216, 172	breqtrrd 4681	. . . . . . . . . 10 $/\$ $/\$ $/\$
218	170, 171, 182, 185, 217	letrd 10194	. . . . . . . . 9 $/\$ $/\$ $/\$
219		elfzle2 12345	. . . . . . . . . . . 12
220	176, 219	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$
221	193	ad2antrr 762	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
222		1re 10039	. . . . . . . . . . . . 13
223		lesubadd 10500	. . . . . . . . . . . . 13 $/\$ $/\$
224	222, 223	mp3an2 1412	. . . . . . . . . . . 12 $/\$
225	187, 221, 224	syl2anc 693	. . . . . . . . . . 11 $/\$ $/\$ $/\$
226	220, 225	mpbird 247	. . . . . . . . . 10 $/\$ $/\$ $/\$
227	172, 226	eqbrtrd 4675	. . . . . . . . 9 $/\$ $/\$ $/\$
228	153	ad2antrr 762	. . . . . . . . . 10 $/\$ $/\$ $/\$
229	138	ad2antrr 762	. . . . . . . . . 10 $/\$ $/\$ $/\$
230	181, 228, 229, 155	syl3anc 1326	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
231	218, 227, 230	mpbir2and 957	. . . . . . . 8 $/\$ $/\$ $/\$
232	171, 182	lenltd 10183	. . . . . . . . . . 11 $/\$ $/\$ $/\$
233	217, 232	mpbid 222	. . . . . . . . . 10 $/\$ $/\$ $/\$
234	233, 53	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$
235	172	oveq1d 6665	. . . . . . . . . . 11 $/\$ $/\$ $/\$
236	178	zcnd 11483	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
237		npcan 10290	. . . . . . . . . . . 12 $/\$
238	236, 114, 237	sylancl 694	. . . . . . . . . . 11 $/\$ $/\$ $/\$
239	235, 238	eqtrd 2656	. . . . . . . . . 10 $/\$ $/\$ $/\$
240	239	fveq2d 6195	. . . . . . . . 9 $/\$ $/\$ $/\$
241	17	ad2antrr 762	. . . . . . . . . 10 $/\$ $/\$ $/\$
242	241, 175, 161	syl2anc 693	. . . . . . . . 9 $/\$ $/\$ $/\$
243	234, 240, 242	3eqtrrd 2661	. . . . . . . 8 $/\$ $/\$ $/\$
244	231, 243	jca 554	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
245	244	expr 643	. . . . . 6 $/\$ $/\$ $/\$
246	168, 245	sylbid 230	. . . . 5 $/\$ $/\$ $/\$
247	166, 246	pm2.61dan 832	. . . 4 $/\$ $/\$
248	247	expimpd 629	. . 3 $/\$ $/\$
249	122, 248	impbid 202	. 2 $/\$ $/\$
250	1, 2, 6, 249	f1od 6885	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

wne 2794

cvv 3200

wss 3574

cif 4086 class class class wbr 4653

cmpt 4729

ccnv 5113

wf 5884

wf1 5885

wf1o 5887

cfv 5888 (class class class)co 6650

cc 9934

cr 9935

c1 9937

caddc 9939

clt 10074

cle 10075

cmin 10266

cz 11377

cuz 11687

cfz 12326

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327

This theorem is referenced by: seqf1olem2 12841

W3C validator