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

Theorem plyeq0lem 20068
 Description: Lemma for plyeq0 20069. If is the coefficient function for a nonzero polynomial such that for every and is the nonzero leading coefficient, then the function is a sum of powers of , and so the limit of this function as is the constant term, . But everywhere, so this limit is also equal to zero so that , a contradiction. (Contributed by Mario Carneiro, 22-Jul-2014.)
Hypotheses
Ref Expression
plyeq0.1
plyeq0.2
plyeq0.3
plyeq0.4
plyeq0.5
plyeq0.6
plyeq0.7
Assertion
Ref Expression
plyeq0lem
Distinct variable groups:   ,,   ,   ,,   ,,   ,,
Allowed substitution hint:   ()

Proof of Theorem plyeq0lem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 10467 . . . . . 6
2 1z 10257 . . . . . . 7
32a1i 11 . . . . . 6
4 fzfid 11253 . . . . . 6
52a1i 11 . . . . . . . . . 10
6 plyeq0.3 . . . . . . . . . . . . . . . . 17
7 plyeq0.1 . . . . . . . . . . . . . . . . . . . 20
8 0cn 9031 . . . . . . . . . . . . . . . . . . . . . 22
98a1i 11 . . . . . . . . . . . . . . . . . . . . 21
109snssd 3900 . . . . . . . . . . . . . . . . . . . 20
117, 10unssd 3480 . . . . . . . . . . . . . . . . . . 19
12 cnex 9018 . . . . . . . . . . . . . . . . . . 19
13 ssexg 4304 . . . . . . . . . . . . . . . . . . 19
1411, 12, 13sylancl 644 . . . . . . . . . . . . . . . . . 18
15 nn0ex 10173 . . . . . . . . . . . . . . . . . 18
16 elmapg 6981 . . . . . . . . . . . . . . . . . 18
1714, 15, 16sylancl 644 . . . . . . . . . . . . . . . . 17
186, 17mpbid 202 . . . . . . . . . . . . . . . 16
19 fss 5553 . . . . . . . . . . . . . . . 16
2018, 11, 19syl2anc 643 . . . . . . . . . . . . . . 15
21 elfznn0 11029 . . . . . . . . . . . . . . 15
22 ffvelrn 5821 . . . . . . . . . . . . . . 15
2320, 21, 22syl2an 464 . . . . . . . . . . . . . 14
2423adantr 452 . . . . . . . . . . . . 13
2524abscld 12179 . . . . . . . . . . . 12
2625recnd 9061 . . . . . . . . . . 11
27 divcnv 12574 . . . . . . . . . . 11
2826, 27syl 16 . . . . . . . . . 10
29 nnex 9952 . . . . . . . . . . . 12
3029mptex 5919 . . . . . . . . . . 11
3130a1i 11 . . . . . . . . . 10
32 oveq2 6042 . . . . . . . . . . . . 13
33 eqid 2401 . . . . . . . . . . . . 13
34 ovex 6059 . . . . . . . . . . . . 13
3532, 33, 34fvmpt 5759 . . . . . . . . . . . 12
3635adantl 453 . . . . . . . . . . 11
37 nndivre 9981 . . . . . . . . . . . 12
3825, 37sylan 458 . . . . . . . . . . 11
3936, 38eqeltrd 2475 . . . . . . . . . 10
40 oveq1 6041 . . . . . . . . . . . . . 14
4140oveq2d 6050 . . . . . . . . . . . . 13
42 eqid 2401 . . . . . . . . . . . . 13
43 ovex 6059 . . . . . . . . . . . . 13
4441, 42, 43fvmpt 5759 . . . . . . . . . . . 12
4544adantl 453 . . . . . . . . . . 11
4623ad2antrr 707 . . . . . . . . . . . . 13
4746abscld 12179 . . . . . . . . . . . 12
48 nnrp 10567 . . . . . . . . . . . . . . 15
4948adantl 453 . . . . . . . . . . . . . 14
50 elfzelz 11005 . . . . . . . . . . . . . . . 16
51 cnvimass 5178 . . . . . . . . . . . . . . . . . . 19
52 fdm 5549 . . . . . . . . . . . . . . . . . . . 20
5318, 52syl 16 . . . . . . . . . . . . . . . . . . 19
5451, 53syl5sseq 3353 . . . . . . . . . . . . . . . . . 18
55 plyeq0.6 . . . . . . . . . . . . . . . . . . 19
56 nn0ssz 10248 . . . . . . . . . . . . . . . . . . . . 21
5754, 56syl6ss 3317 . . . . . . . . . . . . . . . . . . . 20
58 plyeq0.7 . . . . . . . . . . . . . . . . . . . 20
59 plyeq0.2 . . . . . . . . . . . . . . . . . . . . . 22
6059nn0red 10221 . . . . . . . . . . . . . . . . . . . . 21
6154sselda 3305 . . . . . . . . . . . . . . . . . . . . . . 23
62 plyeq0.4 . . . . . . . . . . . . . . . . . . . . . . . . 25
63 plyco0 20050 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6459, 20, 63syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25
6562, 64mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . 24
6665adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
67 ffn 5545 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6818, 67syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
69 elpreima 5803 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7068, 69syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
7170simplbda 608 . . . . . . . . . . . . . . . . . . . . . . . 24
72 eldifsni 3885 . . . . . . . . . . . . . . . . . . . . . . . 24
7371, 72syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
74 fveq2 5682 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7574neeq1d 2577 . . . . . . . . . . . . . . . . . . . . . . . . 25
76 breq1 4170 . . . . . . . . . . . . . . . . . . . . . . . . 25
7775, 76imbi12d 312 . . . . . . . . . . . . . . . . . . . . . . . 24
7877rspcv 3005 . . . . . . . . . . . . . . . . . . . . . . 23
7961, 66, 73, 78syl3c 59 . . . . . . . . . . . . . . . . . . . . . 22
8079ralrimiva 2746 . . . . . . . . . . . . . . . . . . . . 21
81 breq2 4171 . . . . . . . . . . . . . . . . . . . . . . 23
8281ralbidv 2683 . . . . . . . . . . . . . . . . . . . . . 22
8382rspcev 3009 . . . . . . . . . . . . . . . . . . . . 21
8460, 80, 83syl2anc 643 . . . . . . . . . . . . . . . . . . . 20
85 suprzcl 10295 . . . . . . . . . . . . . . . . . . . 20
8657, 58, 84, 85syl3anc 1184 . . . . . . . . . . . . . . . . . . 19
8755, 86syl5eqel 2485 . . . . . . . . . . . . . . . . . 18
8854, 87sseldd 3306 . . . . . . . . . . . . . . . . 17
8988nn0zd 10319 . . . . . . . . . . . . . . . 16
90 zsubcl 10265 . . . . . . . . . . . . . . . 16
9150, 89, 90syl2anr 465 . . . . . . . . . . . . . . 15
9291ad2antrr 707 . . . . . . . . . . . . . 14
9349, 92rpexpcld 11487 . . . . . . . . . . . . 13
9493rpred 10594 . . . . . . . . . . . 12
9547, 94remulcld 9063 . . . . . . . . . . 11
9645, 95eqeltrd 2475 . . . . . . . . . 10
97 nnrecre 9982 . . . . . . . . . . . . 13
9897adantl 453 . . . . . . . . . . . 12
9924absge0d 12187 . . . . . . . . . . . . 13
10099adantr 452 . . . . . . . . . . . 12
101 nnre 9953 . . . . . . . . . . . . . . 15
102101adantl 453 . . . . . . . . . . . . . 14
103 nnge1 9972 . . . . . . . . . . . . . . 15
104103adantl 453 . . . . . . . . . . . . . 14
105 1re 9037 . . . . . . . . . . . . . . . . 17
106105a1i 11 . . . . . . . . . . . . . . . 16
10792zred 10321 . . . . . . . . . . . . . . . 16
108 simplr 732 . . . . . . . . . . . . . . . . . . 19
10950adantl 453 . . . . . . . . . . . . . . . . . . . . 21
110109ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20
11189ad3antrrr 711 . . . . . . . . . . . . . . . . . . . 20
112 zltp1le 10271 . . . . . . . . . . . . . . . . . . . 20
113110, 111, 112syl2anc 643 . . . . . . . . . . . . . . . . . . 19
114108, 113mpbid 202 . . . . . . . . . . . . . . . . . 18
11521adantl 453 . . . . . . . . . . . . . . . . . . . . 21
116115nn0red 10221 . . . . . . . . . . . . . . . . . . . 20
117116ad2antrr 707 . . . . . . . . . . . . . . . . . . 19
11888adantr 452 . . . . . . . . . . . . . . . . . . . . 21
119118nn0red 10221 . . . . . . . . . . . . . . . . . . . 20
120119ad2antrr 707 . . . . . . . . . . . . . . . . . . 19
121117, 106, 120leaddsub2d 9574 . . . . . . . . . . . . . . . . . 18
122114, 121mpbid 202 . . . . . . . . . . . . . . . . 17
123116recnd 9061 . . . . . . . . . . . . . . . . . . 19
124123ad2antrr 707 . . . . . . . . . . . . . . . . . 18
125119recnd 9061 . . . . . . . . . . . . . . . . . . 19
126125ad2antrr 707 . . . . . . . . . . . . . . . . . 18
127124, 126negsubdi2d 9373 . . . . . . . . . . . . . . . . 17
128122, 127breqtrrd 4193 . . . . . . . . . . . . . . . 16
129106, 107, 128lenegcon2d 9555 . . . . . . . . . . . . . . 15
130 znegcl 10259 . . . . . . . . . . . . . . . . 17
1312, 130ax-mp 8 . . . . . . . . . . . . . . . 16
132 eluz 10445 . . . . . . . . . . . . . . . 16
13392, 131, 132sylancl 644 . . . . . . . . . . . . . . 15
134129, 133mpbird 224 . . . . . . . . . . . . . 14
135102, 104, 134leexp2ad 11496 . . . . . . . . . . . . 13
136 nncn 9954 . . . . . . . . . . . . . . 15
137136adantl 453 . . . . . . . . . . . . . 14
138 expn1 11332 . . . . . . . . . . . . . 14
139137, 138syl 16 . . . . . . . . . . . . 13
140135, 139breqtrd 4191 . . . . . . . . . . . 12
14194, 98, 47, 100, 140lemul2ad 9897 . . . . . . . . . . 11
14226adantr 452 . . . . . . . . . . . . 13
143 nnne0 9978 . . . . . . . . . . . . . 14
144143adantl 453 . . . . . . . . . . . . 13
145142, 137, 144divrecd 9739 . . . . . . . . . . . 12
14636, 145eqtrd 2433 . . . . . . . . . . 11
147141, 45, 1463brtr4d 4197 . . . . . . . . . 10
14893rpge0d 10598 . . . . . . . . . . . 12
14947, 94, 100, 148mulge0d 9549 . . . . . . . . . . 11
150149, 45breqtrrd 4193 . . . . . . . . . 10
1511, 5, 28, 31, 39, 96, 147, 150climsqz2 12376 . . . . . . . . 9
15229mptex 5919 . . . . . . . . . . 11
153152a1i 11 . . . . . . . . . 10
15440oveq2d 6050 . . . . . . . . . . . . . . 15
155 eqid 2401 . . . . . . . . . . . . . . 15
156 ovex 6059 . . . . . . . . . . . . . . 15
157154, 155, 156fvmpt 5759 . . . . . . . . . . . . . 14
158157ad2antlr 708 . . . . . . . . . . . . 13
15920adantr 452 . . . . . . . . . . . . . . 15
160159, 21, 22syl2an 464 . . . . . . . . . . . . . 14
161136ad2antlr 708 . . . . . . . . . . . . . . 15
162143ad2antlr 708 . . . . . . . . . . . . . . 15
16389adantr 452 . . . . . . . . . . . . . . . 16
16450, 163, 90syl2anr 465 . . . . . . . . . . . . . . 15
165161, 162, 164expclzd 11469 . . . . . . . . . . . . . 14
166160, 165mulcld 9055 . . . . . . . . . . . . 13
167158, 166eqeltrd 2475 . . . . . . . . . . . 12
168167an32s 780 . . . . . . . . . . 11
169168adantlr 696 . . . . . . . . . 10
17094recnd 9061 . . . . . . . . . . . . 13
17146, 170absmuld 12197 . . . . . . . . . . . 12
17294, 148absidd 12166 . . . . . . . . . . . . 13
173172oveq2d 6050 . . . . . . . . . . . 12
174171, 173eqtrd 2433 . . . . . . . . . . 11
175157adantl 453 . . . . . . . . . . . 12
176175fveq2d 5686 . . . . . . . . . . 11
177174, 176, 453eqtr4rd 2444 . . . . . . . . . 10
1781, 5, 153, 31, 169, 177climabs0 12320 . . . . . . . . 9
179151, 178mpbird 224 . . . . . . . 8
180116adantr 452 . . . . . . . . . . 11
181 simpr 448 . . . . . . . . . . 11
182180, 181ltned 9155 . . . . . . . . . 10
183 elsn 3786 . . . . . . . . . . 11
184183necon3bbii 2595 . . . . . . . . . 10
185182, 184sylibr 204 . . . . . . . . 9
186 iffalse 3703 . . . . . . . . 9
187185, 186syl 16 . . . . . . . 8
188179, 187breqtrrd 4193 . . . . . . 7
189 nncn 9954 . . . . . . . . . . . . . . 15
190189ad2antlr 708 . . . . . . . . . . . . . 14
191 nnne0 9978 . . . . . . . . . . . . . . 15
192191ad2antlr 708 . . . . . . . . . . . . . 14
19391ad3antrrr 711 . . . . . . . . . . . . . 14
194190, 192, 193expclzd 11469 . . . . . . . . . . . . 13
195194mul02d 9210 . . . . . . . . . . . 12
196 simpr 448 . . . . . . . . . . . . 13
197196oveq1d 6049 . . . . . . . . . . . 12
198196ifeq1d 3710 . . . . . . . . . . . . 13
199 ifid 3728 . . . . . . . . . . . . 13
200198, 199syl6eq 2449 . . . . . . . . . . . 12
201195, 197, 2003eqtr4d 2443 . . . . . . . . . . 11
20223adantr 452 . . . . . . . . . . . . . 14
203202ad2antrr 707 . . . . . . . . . . . . 13
204203mulid1d 9052 . . . . . . . . . . . 12
205 nn0ssre 10171 . . . . . . . . . . . . . . . . . . . . . . . 24
20654, 205syl6ss 3317 . . . . . . . . . . . . . . . . . . . . . . 23
207206ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22
20858ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22
20984ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22
21021ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . 23
211 ffvelrn 5821 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
21218, 21, 211syl2an 464 . . . . . . . . . . . . . . . . . . . . . . . . . 26
213212anim1i 552 . . . . . . . . . . . . . . . . . . . . . . . . 25
214 eldifsn 3884 . . . . . . . . . . . . . . . . . . . . . . . . 25
215213, 214sylibr 204 . . . . . . . . . . . . . . . . . . . . . . . 24
216 difun2 3664 . . . . . . . . . . . . . . . . . . . . . . . 24
217215, 216syl6eleq 2491 . . . . . . . . . . . . . . . . . . . . . . 23
218 elpreima 5803 . . . . . . . . . . . . . . . . . . . . . . . . 25
21968, 218syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
220219ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . 23
221210, 217, 220mpbir2and 889 . . . . . . . . . . . . . . . . . . . . . 22
222 suprub 9915 . . . . . . . . . . . . . . . . . . . . . 22
223207, 208, 209, 221, 222syl31anc 1187 . . . . . . . . . . . . . . . . . . . . 21
224223, 55syl6breqr 4207 . . . . . . . . . . . . . . . . . . . 20
225224adantlr 696 . . . . . . . . . . . . . . . . . . 19
226225adantlr 696 . . . . . . . . . . . . . . . . . 18
227 simpllr 736 . . . . . . . . . . . . . . . . . 18
228116ad3antrrr 711 . . . . . . . . . . . . . . . . . . 19
229119ad3antrrr 711 . . . . . . . . . . . . . . . . . . 19
230228, 229letri3d 9161 . . . . . . . . . . . . . . . . . 18
231226, 227, 230mpbir2and 889 . . . . . . . . . . . . . . . . 17
232231oveq1d 6049 . . . . . . . . . . . . . . . 16
233125ad3antrrr 711 . . . . . . . . . . . . . . . . 17
234233subidd 9345 . . . . . . . . . . . . . . . 16
235232, 234eqtrd 2433 . . . . . . . . . . . . . . 15
236235oveq2d 6050 . . . . . . . . . . . . . 14
237189ad2antlr 708 . . . . . . . . . . . . . . 15
238237exp0d 11458 . . . . . . . . . . . . . 14
239236, 238eqtrd 2433 . . . . . . . . . . . . 13
240239oveq2d 6050 . . . . . . . . . . . 12
241231, 183sylibr 204 . . . . . . . . . . . . 13
242 iftrue 3702 . . . . . . . . . . . . 13
243241, 242syl 16 . . . . . . . . . . . 12
244204, 240, 2433eqtr4d 2443 . . . . . . . . . . 11
245201, 244pm2.61dane 2642 . . . . . . . . . 10
246245mpteq2dva 4250 . . . . . . . . 9
247 fconstmpt 4875 . . . . . . . . 9
248246, 247syl6eqr 2451 . . . . . . . 8
249 ifcl 3732 . . . . . . . . . 10
250202, 8, 249sylancl 644 . . . . . . . . 9
2511eqimss2i 3360 . . . . . . . . . 10
252251, 29climconst2 12283 . . . . . . . . 9
253250, 2, 252sylancl 644 . . . . . . . 8
254248, 253eqbrtrd 4187 . . . . . . 7
255188, 254, 116, 119ltlecasei 9128 . . . . . 6
256 snex 4360 . . . . . . . 8
25729, 256xpex 4944 . . . . . . 7
258257a1i 11 . . . . . 6
259168anasss 629 . . . . . 6
260 plyeq0.5 . . . . . . . . . . . 12
261260fveq1d 5684 . . . . . . . . . . 11
262261adantr 452 . . . . . . . . . 10
263136adantl 453 . . . . . . . . . . 11
264 0pval 19502 . . . . . . . . . . 11
265263, 264syl 16 . . . . . . . . . 10
266 oveq1 6041 . . . . . . . . . . . . . 14
267266oveq2d 6050 . . . . . . . . . . . . 13
268267sumeq2sdv 12439 . . . . . . . . . . . 12
269 eqid 2401 . . . . . . . . . . . 12
270 sumex 12422 . . . . . . . . . . . 12
271268, 269, 270fvmpt 5759 . . . . . . . . . . 11
272263, 271syl 16 . . . . . . . . . 10
273262, 265, 2723eqtr3d 2441 . . . . . . . . 9
274273oveq1d 6049 . . . . . . . 8
275 expcl 11340 . . . . . . . . . 10
276136, 88, 275syl2anr 465 . . . . . . . . 9
277143adantl 453 . . . . . . . . . 10
278263, 277, 163expne0d 11470 . . . . . . . . 9
279276, 278div0d 9735 . . . . . . . 8
280 fzfid 11253 . . . . . . . . 9
281 expcl 11340 . . . . . . . . . . 11
282263, 21, 281syl2an 464 . . . . . . . . . 10
283160, 282mulcld 9055 . . . . . . . . 9
284280, 276, 283, 278fsumdivc 12510 . . . . . . . 8
285274, 279, 2843eqtr3d 2441 . . . . . . 7
286 fvconst2g 5898 . . . . . . . 8
2879, 286sylan 458 . . . . . . 7
288163adantr 452 . . . . . . . . . . 11
28950adantl 453 . . . . . . . . . . 11
290161, 162, 288, 289expsubd 11475 . . . . . . . . . 10
291290oveq2d 6050 . . . . . . . . 9
292276adantr 452 . . . . . . . . . 10
293278adantr 452 . . . . . . . . . 10
294160, 282, 292, 293divassd 9771 . . . . . . . . 9
295291, 158, 2943eqtr4d 2443 . . . . . . . 8
296295sumeq2dv 12438 . . . . . . 7
297285, 287, 2963eqtr4d 2443 . . . . . 6
2981, 3, 4, 255, 258, 259, 297climfsum 12540 . . . . 5
299 suprleub 9918 . . . . . . . . . . . 12
300206, 58, 84, 60, 299syl31anc 1187 . . . . . . . . . . 11
30180, 300mpbird 224 . . . . . . . . . 10
30255, 301syl5eqbr 4200 . . . . . . . . 9
303 nn0uz 10466 . . . . . . . . . . 11
30488, 303syl6eleq 2491 . . . . . . . . . 10
30559nn0zd 10319 . . . . . . . . . 10
306 elfz5 10997 . . . . . . . . . 10
307304, 305, 306syl2anc 643 . . . . . . . . 9
308302, 307mpbird 224 . . . . . . . 8
309308snssd 3900 . . . . . . 7
31020, 88ffvelrnd 5824 . . . . . . . . 9
311 elsni 3795 . . . . . . . . . . 11
312311fveq2d 5686 . . . . . . . . . 10
313312eleq1d 2467 . . . . . . . . 9
314310, 313syl5ibrcom 214 . . . . . . . 8
315314ralrimiv 2745 . . . . . . 7
3164olcd 383 . . . . . . 7
317 sumss2 12461 . . . . . . 7
318309, 315, 316, 317syl21anc 1183 . . . . . 6
319 ltso 9103 . . . . . . . . 9
320319supex 7415 . . . . . . . 8
32155, 320eqeltri 2471 . . . . . . 7
322 fveq2 5682 . . . . . . . 8
323322sumsn 12475 . . . . . . 7
324321, 310, 323sylancr 645 . . . . . 6
325318, 324eqtr3d 2435 . . . . 5
326298, 325breqtrd 4191 . . . 4
327251, 29climconst2 12283 . . . . 5
3288, 2, 327mp2an 654 . . . 4
329 climuni 12287 . . . 4
330326, 328, 329sylancl 644 . . 3
331 fvex 5696 . . . 4
332331elsnc 3794 . . 3
333330, 332sylibr 204 . 2
334 elpreima 5803 . . . . . 6
33568, 334syl 16 . . . . 5
33687, 335mpbid 202 . . . 4
337336simprd 450 . . 3
338337eldifbd 3290 . 2
339333, 338pm2.65i 167 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wo 358   wa 359   wceq 1649   wcel 1721   wne 2564  wral 2663  wrex 2664  cvv 2913   cdif 3274   cun 3275   wss 3277  c0 3585  cif 3696  csn 3771   class class class wbr 4167   cmpt 4221   cxp 4830  ccnv 4831   cdm 4832  cima 4835   wfn 5403  wf 5404  cfv 5408  (class class class)co 6034   cmap 6968  cfn 7059  csup 7394  cc 8935  cr 8936  cc0 8937  c1 8938   caddc 8940   cmul 8942   clt 9067   cle 9068   cmin 9237  cneg 9238   cdiv 9623  cn 9946  cn0 10167  cz 10228  cuz 10434  crp 10558  cfz 10989  cexp 11323  cabs 11980   cli 12219  csu 12420  c0p 19500 This theorem is referenced by:  plyeq0  20069 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-rep 4275  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655  ax-inf2 7543  ax-cnex 8993  ax-resscn 8994  ax-1cn 8995  ax-icn 8996  ax-addcl 8997  ax-addrcl 8998  ax-mulcl 8999  ax-mulrcl 9000  ax-mulcom 9001  ax-addass 9002  ax-mulass 9003  ax-distr 9004  ax-i2m1 9005  ax-1ne0 9006  ax-1rid 9007  ax-rnegex 9008  ax-rrecex 9009  ax-cnre 9010  ax-pre-lttri 9011  ax-pre-lttrn 9012  ax-pre-ltadd 9013  ax-pre-mulgt0 9014  ax-pre-sup 9015  ax-addf 9016 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-nel 2567  df-ral 2668  df-rex 2669  df-reu 2670  df-rmo 2671  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-uni 3972  df-int 4007  df-iun 4051  df-br 4168  df-opab 4222  df-mpt 4223  df-tr 4258  df-eprel 4449  df-id 4453  df-po 4458  df-so 4459  df-fr 4496  df-se 4497  df-we 4498  df-ord 4539  df-on 4540  df-lim 4541  df-suc 4542  df-om 4800  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-isom 5417  df-ov 6037  df-oprab 6038  df-mpt2 6039  df-1st 6302  df-2nd 6303  df-riota 6499  df-recs 6583  df-rdg 6618  df-1o 6674  df-oadd 6678  df-er 6855  df-map 6970  df-pm 6971  df-en 7060  df-dom 7061  df-sdom 7062  df-fin 7063  df-sup 7395  df-oi 7426  df-card 7773  df-pnf 9069  df-mnf 9070  df-xr 9071  df-ltxr 9072  df-le 9073  df-sub 9239  df-neg 9240  df-div 9624  df-nn 9947  df-2 10004  df-3 10005  df-n0 10168  df-z 10229  df-uz 10435  df-rp 10559  df-fz 10990  df-fzo 11080  df-fl 11143  df-seq 11265  df-exp 11324  df-hash 11560  df-cj 11845  df-re 11846  df-im 11847  df-sqr 11981  df-abs 11982  df-clim 12223  df-rlim 12224  df-sum 12421  df-0p 19501
 Copyright terms: Public domain W3C validator