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

Theorem ftalem5OLD 24082
 Description: Lemma for fta 24085: Main proof. We have already shifted the minimum found in ftalem3 24078 to zero by a change of variables, and now we show that the minimum value is zero. Expanding in a series about the minimum value, let be the lowest term in the polynomial that is nonzero, and let be a -th root of . Then an evaluation of where is a sufficiently small positive number yields for the first term and for the -th term, and all higher terms are bounded because is small. Thus, , in contradiction to our choice of as the minimum. (Contributed by Mario Carneiro, 14-Sep-2014.) Obsolete version of ftalem5 24080 as of 1-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
ftalem.1 coeff
ftalem.2 deg
ftalem.3 Poly
ftalem.4
ftalem4OLD.5
ftalem4OLD.6
ftalem4OLD.7
ftalem4OLD.8
ftalem4OLD.9
Assertion
Ref Expression
ftalem5OLD
Distinct variable groups:   ,,,   ,,   ,,,   ,,,   ,,   ,   ,,   ,   ,,,
Allowed substitution hints:   ()   (,)   ()   (,)   ()

Proof of Theorem ftalem5OLD
StepHypRef Expression
1 ftalem.1 . . . . . 6 coeff
2 ftalem.2 . . . . . 6 deg
3 ftalem.3 . . . . . 6 Poly
4 ftalem.4 . . . . . 6
5 ftalem4OLD.5 . . . . . 6
6 ftalem4OLD.6 . . . . . 6
7 ftalem4OLD.7 . . . . . 6
8 ftalem4OLD.8 . . . . . 6
9 ftalem4OLD.9 . . . . . 6
101, 2, 3, 4, 5, 6, 7, 8, 9ftalem4OLD 24081 . . . . 5
1110simprd 470 . . . 4
1211simp1d 1042 . . 3
1311simp3d 1044 . . . . 5
1413rpred 11364 . . . 4
1514recnd 9687 . . 3
1612, 15mulcld 9681 . 2
17 plyf 23231 . . . . . 6 Poly
183, 17syl 17 . . . . 5
1918, 16ffvelrnd 6038 . . . 4
2019abscld 13575 . . 3
21 0cn 9653 . . . . . . 7
22 ffvelrn 6035 . . . . . . 7
2318, 21, 22sylancl 675 . . . . . 6
2423abscld 13575 . . . . 5
2510simpld 466 . . . . . . . . 9
2625simpld 466 . . . . . . . 8
2726nnnn0d 10949 . . . . . . 7
2814, 27reexpcld 12471 . . . . . 6
2924, 28remulcld 9689 . . . . 5
3024, 29resubcld 10068 . . . 4
31 fzfid 12224 . . . . . 6
32 peano2nn0 10934 . . . . . . . . . 10
3327, 32syl 17 . . . . . . . . 9
34 elfzuz 11822 . . . . . . . . 9
35 eluznn0 11251 . . . . . . . . 9
3633, 34, 35syl2an 485 . . . . . . . 8
371coef3 23265 . . . . . . . . . 10 Poly
383, 37syl 17 . . . . . . . . 9
39 ffvelrn 6035 . . . . . . . . 9
4038, 39sylan 479 . . . . . . . 8
4136, 40syldan 478 . . . . . . 7
4216adantr 472 . . . . . . . 8
4342, 36expcld 12454 . . . . . . 7
4441, 43mulcld 9681 . . . . . 6
4531, 44fsumcl 13876 . . . . 5
4645abscld 13575 . . . 4
4730, 46readdcld 9688 . . 3
48 fzfid 12224 . . . . . 6
49 elfznn0 11913 . . . . . . . 8
5038, 49, 39syl2an 485 . . . . . . 7
51 expcl 12328 . . . . . . . 8
5216, 49, 51syl2an 485 . . . . . . 7
5350, 52mulcld 9681 . . . . . 6
5448, 53fsumcl 13876 . . . . 5
5554, 45abstrid 13595 . . . 4
561, 2coeid2 23272 . . . . . . 7 Poly
573, 16, 56syl2anc 673 . . . . . 6
5826nnred 10646 . . . . . . . . 9
5958ltp1d 10559 . . . . . . . 8
60 fzdisj 11852 . . . . . . . 8
6159, 60syl 17 . . . . . . 7
62 ssrab2 3500 . . . . . . . . . . . 12
63 nnuz 11218 . . . . . . . . . . . 12
6462, 63sseqtri 3450 . . . . . . . . . . 11
654nnne0d 10676 . . . . . . . . . . . . 13
662, 1dgreq0 23298 . . . . . . . . . . . . . . . 16 Poly
673, 66syl 17 . . . . . . . . . . . . . . 15
68 fveq2 5879 . . . . . . . . . . . . . . . . 17 deg deg
69 dgr0 23295 . . . . . . . . . . . . . . . . 17 deg
7068, 69syl6eq 2521 . . . . . . . . . . . . . . . 16 deg
712, 70syl5eq 2517 . . . . . . . . . . . . . . 15
7267, 71syl6bir 237 . . . . . . . . . . . . . 14
7372necon3d 2664 . . . . . . . . . . . . 13
7465, 73mpd 15 . . . . . . . . . . . 12
75 fveq2 5879 . . . . . . . . . . . . . 14
7675neeq1d 2702 . . . . . . . . . . . . 13
7776elrab 3184 . . . . . . . . . . . 12
784, 74, 77sylanbrc 677 . . . . . . . . . . 11
79 infmssuzleOLD 11269 . . . . . . . . . . 11
8064, 78, 79sylancr 676 . . . . . . . . . 10
816, 80syl5eqbr 4429 . . . . . . . . 9
82 nn0uz 11217 . . . . . . . . . . 11
8327, 82syl6eleq 2559 . . . . . . . . . 10
844nnzd 11062 . . . . . . . . . 10
85 elfz5 11818 . . . . . . . . . 10
8683, 84, 85syl2anc 673 . . . . . . . . 9
8781, 86mpbird 240 . . . . . . . 8
88 fzsplit 11851 . . . . . . . 8
8987, 88syl 17 . . . . . . 7
90 fzfid 12224 . . . . . . 7
91 elfznn0 11913 . . . . . . . . 9
9238, 91, 39syl2an 485 . . . . . . . 8
9316, 91, 51syl2an 485 . . . . . . . 8
9492, 93mulcld 9681 . . . . . . 7
9561, 89, 90, 94fsumsplit 13883 . . . . . 6
9657, 95eqtrd 2505 . . . . 5
9796fveq2d 5883 . . . 4
981coefv0 23281 . . . . . . . . . . . . 13 Poly
993, 98syl 17 . . . . . . . . . . . 12
10099eqcomd 2477 . . . . . . . . . . 11
10116exp0d 12448 . . . . . . . . . . 11
102100, 101oveq12d 6326 . . . . . . . . . 10
10323mulid1d 9678 . . . . . . . . . 10
104102, 103eqtrd 2505 . . . . . . . . 9
105 1e0p1 11102 . . . . . . . . . . . . 13
106105oveq1i 6318 . . . . . . . . . . . 12
107106sumeq1i 13841 . . . . . . . . . . 11
10826, 63syl6eleq 2559 . . . . . . . . . . . 12
109 elfznn 11854 . . . . . . . . . . . . . . 15
110109nnnn0d 10949 . . . . . . . . . . . . . 14
11138, 110, 39syl2an 485 . . . . . . . . . . . . 13
11216, 110, 51syl2an 485 . . . . . . . . . . . . 13
113111, 112mulcld 9681 . . . . . . . . . . . 12
114 fveq2 5879 . . . . . . . . . . . . 13
115 oveq2 6316 . . . . . . . . . . . . 13
116114, 115oveq12d 6326 . . . . . . . . . . . 12
117108, 113, 116fsumm1 13889 . . . . . . . . . . 11
118107, 117syl5eqr 2519 . . . . . . . . . 10
119 elfznn 11854 . . . . . . . . . . . . . . . . . . . . 21
120119adantl 473 . . . . . . . . . . . . . . . . . . . 20
121120nnred 10646 . . . . . . . . . . . . . . . . . . 19
12258adantr 472 . . . . . . . . . . . . . . . . . . . 20
123 peano2rem 9961 . . . . . . . . . . . . . . . . . . . 20
124122, 123syl 17 . . . . . . . . . . . . . . . . . . 19
125 elfzle2 11829 . . . . . . . . . . . . . . . . . . . 20
126125adantl 473 . . . . . . . . . . . . . . . . . . 19
127122ltm1d 10561 . . . . . . . . . . . . . . . . . . 19
128121, 124, 122, 126, 127lelttrd 9810 . . . . . . . . . . . . . . . . . 18
129121, 122ltnled 9799 . . . . . . . . . . . . . . . . . 18
130128, 129mpbid 215 . . . . . . . . . . . . . . . . 17
131 infmssuzleOLD 11269 . . . . . . . . . . . . . . . . . . 19
1326, 131syl5eqbr 4429 . . . . . . . . . . . . . . . . . 18
13364, 132mpan 684 . . . . . . . . . . . . . . . . 17
134130, 133nsyl 125 . . . . . . . . . . . . . . . 16
135 fveq2 5879 . . . . . . . . . . . . . . . . . . . 20
136135neeq1d 2702 . . . . . . . . . . . . . . . . . . 19
137136elrab3 3185 . . . . . . . . . . . . . . . . . 18
138120, 137syl 17 . . . . . . . . . . . . . . . . 17
139138necon2bbid 2686 . . . . . . . . . . . . . . . 16
140134, 139mpbird 240 . . . . . . . . . . . . . . 15
141140oveq1d 6323 . . . . . . . . . . . . . 14
142119nnnn0d 10949 . . . . . . . . . . . . . . . 16
14316, 142, 51syl2an 485 . . . . . . . . . . . . . . 15
144143mul02d 9849 . . . . . . . . . . . . . 14
145141, 144eqtrd 2505 . . . . . . . . . . . . 13
146145sumeq2dv 13846 . . . . . . . . . . . 12
147 fzfi 12223 . . . . . . . . . . . . . 14
148147olci 398 . . . . . . . . . . . . 13
149 sumz 13865 . . . . . . . . . . . . 13
150148, 149ax-mp 5 . . . . . . . . . . . 12
151146, 150syl6eq 2521 . . . . . . . . . . 11
15212, 15, 27mulexpd 12469 . . . . . . . . . . . . . 14
153152oveq2d 6324 . . . . . . . . . . . . 13
15438, 27ffvelrnd 6038 . . . . . . . . . . . . . 14
15512, 27expcld 12454 . . . . . . . . . . . . . 14
15628recnd 9687 . . . . . . . . . . . . . 14
157154, 155, 156mulassd 9684 . . . . . . . . . . . . 13
158153, 157eqtr4d 2508 . . . . . . . . . . . 12
1597oveq1i 6318 . . . . . . . . . . . . . . . 16
16058recnd 9687 . . . . . . . . . . . . . . . . . . 19
16126nnne0d 10676 . . . . . . . . . . . . . . . . . . 19
162160, 161recid2d 10401 . . . . . . . . . . . . . . . . . 18
163162oveq2d 6324 . . . . . . . . . . . . . . . . 17
16425simprd 470 . . . . . . . . . . . . . . . . . . . 20
16523, 154, 164divcld 10405 . . . . . . . . . . . . . . . . . . 19
166165negcld 9992 . . . . . . . . . . . . . . . . . 18
16726nnrecred 10677 . . . . . . . . . . . . . . . . . . 19
168167recnd 9687 . . . . . . . . . . . . . . . . . 18
169166, 168, 27cxpmul2d 23733 . . . . . . . . . . . . . . . . 17
170166cxp1d 23730 . . . . . . . . . . . . . . . . 17
171163, 169, 1703eqtr3d 2513 . . . . . . . . . . . . . . . 16
172159, 171syl5eq 2517 . . . . . . . . . . . . . . 15
173172oveq2d 6324 . . . . . . . . . . . . . 14
174154, 165mulneg2d 10093 . . . . . . . . . . . . . 14
17523, 154, 164divcan2d 10407 . . . . . . . . . . . . . . 15
176175negeqd 9889 . . . . . . . . . . . . . 14
177173, 174, 1763eqtrd 2509 . . . . . . . . . . . . 13
178177oveq1d 6323 . . . . . . . . . . . 12
17923, 156mulneg1d 10092 . . . . . . . . . . . 12
180158, 178, 1793eqtrd 2509 . . . . . . . . . . 11
181151, 180oveq12d 6326 . . . . . . . . . 10
18223, 156mulcld 9681 . . . . . . . . . . . 12
183182negcld 9992 . . . . . . . . . . 11
184183addid2d 9852 . . . . . . . . . 10
185118, 181, 1843eqtrd 2509 . . . . . . . . 9
186104, 185oveq12d 6326 . . . . . . . 8
187 fveq2 5879 . . . . . . . . . 10
188 oveq2 6316 . . . . . . . . . 10
189187, 188oveq12d 6326 . . . . . . . . 9
19083, 53, 189fsum1p 13891 . . . . . . . 8
191103oveq1d 6323 . . . . . . . . 9
192 1cnd 9677 . . . . . . . . . 10
19323, 192, 156subdid 10095 . . . . . . . . 9
19423, 182negsubd 10011 . . . . . . . . 9
195191, 193, 1943eqtr4d 2515 . . . . . . . 8
196186, 190, 1953eqtr4d 2515 . . . . . . 7
197196fveq2d 5883 . . . . . 6
198 1re 9660 . . . . . . . . 9
199 resubcl 9958 . . . . . . . . 9
200198, 28, 199sylancr 676 . . . . . . . 8
201200recnd 9687 . . . . . . 7
20223, 201absmuld 13593 . . . . . 6
20313rpge0d 11368 . . . . . . . . . . 11
20411simp2d 1043 . . . . . . . . . . . . . 14
205204rpred 11364 . . . . . . . . . . . . 13
206 min1 11506 . . . . . . . . . . . . 13
207198, 205, 206sylancr 676 . . . . . . . . . . . 12
2089, 207syl5eqbr 4429 . . . . . . . . . . 11
209 exple1 12370 . . . . . . . . . . 11
21014, 203, 208, 27, 209syl31anc 1295 . . . . . . . . . 10
211 subge0 10148 . . . . . . . . . . 11
212198, 28, 211sylancr 676 . . . . . . . . . 10
213210, 212mpbird 240 . . . . . . . . 9
214200, 213absidd 13561 . . . . . . . 8
215214oveq2d 6324 . . . . . . 7
21624recnd 9687 . . . . . . . 8
217216, 192, 156subdid 10095 . . . . . . 7
218216mulid1d 9678 . . . . . . . 8
219218oveq1d 6323 . . . . . . 7
220215, 217, 2193eqtrd 2509 . . . . . 6
221197, 202, 2203eqtrrd 2510 . . . . 5
222221oveq1d 6323 . . . 4
22355, 97, 2223brtr4d 4426 . . 3
22444abscld 13575 . . . . . . 7
22531, 224fsumrecl 13877 . . . . . 6
22631, 44fsumabs 13938 . . . . . 6
227 expcl 12328 . . . . . . . . . . . . 13
22812, 227sylan 479 . . . . . . . . . . . 12
22936, 228syldan 478 . . . . . . . . . . 11
23041, 229mulcld 9681 . . . . . . . . . 10
231230abscld 13575 . . . . . . . . 9
23231, 231fsumrecl 13877 . . . . . . . 8
23314, 33reexpcld 12471 . . . . . . . 8
234232, 233remulcld 9689 . . . . . . 7
235233adantr 472 . . . . . . . . . 10
236231, 235remulcld 9689 . . . . . . . . 9
23712adantr 472 . . . . . . . . . . . . . . 15
23815adantr 472 . . . . . . . . . . . . . . 15
239237, 238, 36mulexpd 12469 . . . . . . . . . . . . . 14
240239oveq2d 6324 . . . . . . . . . . . . 13
24114adantr 472 . . . . . . . . . . . . . . . 16
242241, 36reexpcld 12471 . . . . . . . . . . . . . . 15
243242recnd 9687 . . . . . . . . . . . . . 14
24441, 229, 243mulassd 9684 . . . . . . . . . . . . 13
245240, 244eqtr4d 2508 . . . . . . . . . . . 12
246245fveq2d 5883 . . . . . . . . . . 11
247230, 243absmuld 13593 . . . . . . . . . . 11
248 elfzelz 11826 . . . . . . . . . . . . . . 15
249 rpexpcl 12329 . . . . . . . . . . . . . . 15
25013, 248, 249syl2an 485 . . . . . . . . . . . . . 14
251250rpge0d 11368 . . . . . . . . . . . . 13
252242, 251absidd 13561 . . . . . . . . . . . 12
253252oveq2d 6324 . . . . . . . . . . 11
254246, 247, 2533eqtrd 2509 . . . . . . . . . 10
255230absge0d 13583 . . . . . . . . . . 11
25633adantr 472 . . . . . . . . . . . 12
25734adantl 473 . . . . . . . . . . . 12
258203adantr 472 . . . . . . . . . . . 12
259208adantr 472 . . . . . . . . . . . 12
260241, 256, 257, 258, 259leexp2rd 12487 . . . . . . . . . . 11
261242, 235, 231, 255, 260lemul2ad 10569 . . . . . . . . . 10
262254, 261eqbrtrd 4416 . . . . . . . . 9
26331, 224, 236, 262fsumle 13936 . . . . . . . 8
264233recnd 9687 . . . . . . . . 9
265231recnd 9687 . . . . . . . . 9
26631, 264, 265fsummulc1 13923 . . . . . . . 8
267263, 266breqtrrd 4422 . . . . . . 7
26815, 27expp1d 12455 . . . . . . . . . . 11
269156, 15mulcomd 9682 . . . . . . . . . . 11
270268, 269eqtrd 2505 . . . . . . . . . 10
271270oveq2d 6324 . . . . . . . . 9
272232recnd 9687 . . . . . . . . . 10
273272, 15, 156mulassd 9684 . . . . . . . . 9
274271, 273eqtr4d 2508 . . . . . . . 8
275232, 14remulcld 9689 . . . . . . . . 9
276 nnssz 10981 . . . . . . . . . . . 12
27762, 276sstri 3427 . . . . . . . . . . 11
278 ne0i 3728 . . . . . . . . . . . . . 14
27978, 278syl 17 . . . . . . . . . . . . 13
280 infmssuzclOLD 11270 . . . . . . . . . . . . 13
28164, 279, 280sylancr 676 . . . . . . . . . . . 12
2826, 281syl5eqel 2553 . . . . . . . . . . 11
283277, 282sseldi 3416 . . . . . . . . . 10
28413, 283rpexpcld 12477 . . . . . . . . 9
285 peano2re 9824 . . . . . . . . . . . 12
286232, 285syl 17 . . . . . . . . . . 11
287286, 14remulcld 9689 . . . . . . . . . 10
288232ltp1d 10559 . . . . . . . . . . 11
289232, 286, 13, 288ltmul1dd 11416 . . . . . . . . . 10
290 min2 11507 . . . . . . . . . . . . . 14
291198, 205, 290sylancr 676 . . . . . . . . . . . . 13
2929, 291syl5eqbr 4429 . . . . . . . . . . . 12
293292, 8syl6breq 4435 . . . . . . . . . . 11
294 0red 9662 . . . . . . . . . . . . 13
29531, 231, 255fsumge0 13932 . . . . . . . . . . . . 13
296294, 232, 286, 295, 288lelttrd 9810 . . . . . . . . . . . 12
297 lemuldiv2 10509 . . . . . . . . . . . 12
29814, 24, 286, 296, 297syl112anc 1296 . . . . . . . . . . 11
299293, 298mpbird 240 . . . . . . . . . 10
300275, 287, 24, 289, 299ltletrd 9812 . . . . . . . . 9
301275, 24, 284, 300ltmul1dd 11416 . . . . . . . 8
302274, 301eqbrtrd 4416 . . . . . . 7
303225, 234, 29, 267, 302lelttrd 9810 . . . . . 6
30446, 225, 29, 226, 303lelttrd 9810 . . . . 5
30546, 29, 24, 304ltsub2dd 10247 . . . 4
30630, 46, 24ltaddsubd 10234 . . . 4
307305, 306mpbird 240 . . 3
30820, 47, 24, 223, 307lelttrd 9810 . 2
309 fveq2 5879 . . . . 5
310309fveq2d 5883 . . . 4
311310breq1d 4405 . . 3
312311rspcev 3136 . 2
31316, 308, 312syl2anc 673 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wo 375   wa 376   w3a 1007   wceq 1452   wcel 1904   wne 2641  wrex 2757  crab 2760   cun 3388   cin 3389   wss 3390  c0 3722  cif 3872   class class class wbr 4395  ccnv 4838  wf 5585  cfv 5589  (class class class)co 6308  cfn 7587  csup 7972  cc 9555  cr 9556  cc0 9557  c1 9558   caddc 9560   cmul 9562   clt 9693   cle 9694   cmin 9880  cneg 9881   cdiv 10291  cn 10631  cn0 10893  cz 10961  cuz 11182  crp 11325  cfz 11810  cexp 12310  cabs 13374  csu 13829  c0p 22706  Polycply 23217  coeffccoe 23219  degcdgr 23220   ccxp 23584 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635  ax-addf 9636  ax-mulf 9637 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-om 6712  df-1st 6812  df-2nd 6813  df-supp 6934  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-ixp 7541  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fsupp 7902  df-fi 7943  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-4 10692  df-5 10693  df-6 10694  df-7 10695  df-8 10696  df-9 10697  df-10 10698  df-n0 10894  df-z 10962  df-dec 11075  df-uz 11183  df-q 11288  df-rp 11326  df-xneg 11432  df-xadd 11433  df-xmul 11434  df-ioo 11664  df-ioc 11665  df-ico 11666  df-icc 11667  df-fz 11811  df-fzo 11943  df-fl 12061  df-mod 12130  df-seq 12252  df-exp 12311  df-fac 12498  df-bc 12526  df-hash 12554  df-shft 13207  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-limsup 13603  df-clim 13629  df-rlim 13630  df-sum 13830  df-ef 14198  df-sin 14200  df-cos 14201  df-pi 14203  df-struct 15201  df-ndx 15202  df-slot 15203  df-base 15204  df-sets 15205  df-ress 15206  df-plusg 15281  df-mulr 15282  df-starv 15283  df-sca 15284  df-vsca 15285  df-ip 15286  df-tset 15287  df-ple 15288  df-ds 15290  df-unif 15291  df-hom 15292  df-cco 15293  df-rest 15399  df-topn 15400  df-0g 15418  df-gsum 15419  df-topgen 15420  df-pt 15421  df-prds 15424  df-xrs 15478  df-qtop 15484  df-imas 15485  df-xps 15488  df-mre 15570  df-mrc 15571  df-acs 15573  df-mgm 16566  df-sgrp 16605  df-mnd 16615  df-submnd 16661  df-mulg 16754  df-cntz 17049  df-cmn 17510  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042  df-mopn 19043  df-fbas 19044  df-fg 19045  df-cnfld 19048  df-top 19998  df-bases 19999  df-topon 20000  df-topsp 20001  df-cld 20111  df-ntr 20112  df-cls 20113  df-nei 20191  df-lp 20229  df-perf 20230  df-cn 20320  df-cnp 20321  df-haus 20408  df-tx 20654  df-hmeo 20847  df-fil 20939  df-fm 21031  df-flim 21032  df-flf 21033  df-xms 21413  df-ms 21414  df-tms 21415  df-cncf 21988  df-0p 22707  df-limc 22900  df-dv 22901  df-ply 23221  df-coe 23223  df-dgr 23224  df-log 23585  df-cxp 23586 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator