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

Theorem ftalem2 22296
 Description: Lemma for fta 22302. There exists some such that has magnitude greater than outside the closed ball B(0,r). (Contributed by Mario Carneiro, 14-Sep-2014.)
Hypotheses
Ref Expression
ftalem.1 coeff
ftalem.2 deg
ftalem.3 Poly
ftalem.4
ftalem2.5
ftalem2.6
Assertion
Ref Expression
ftalem2
Distinct variable groups:   ,,,   ,,,   ,,,   ,,   ,   ,,   ,,
Allowed substitution hints:   ()   (,)   ()   ()

Proof of Theorem ftalem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ftalem.1 . . 3 coeff
2 ftalem.2 . . 3 deg
3 ftalem.3 . . 3 Poly
4 ftalem.4 . . 3
51coef3 21585 . . . . . . 7 Poly
63, 5syl 16 . . . . . 6
74nnnn0d 10624 . . . . . 6
86, 7ffvelrnd 5832 . . . . 5
94nnne0d 10354 . . . . . 6
102, 1dgreq0 21617 . . . . . . . . 9 Poly
11 fveq2 5679 . . . . . . . . . . 11 deg deg
12 dgr0 21614 . . . . . . . . . . 11 deg
1311, 12syl6eq 2481 . . . . . . . . . 10 deg
142, 13syl5eq 2477 . . . . . . . . 9
1510, 14syl6bir 229 . . . . . . . 8 Poly
163, 15syl 16 . . . . . . 7
1716necon3d 2636 . . . . . 6
189, 17mpd 15 . . . . 5
198, 18absrpcld 12918 . . . 4
2019rphalfcld 11027 . . 3
21 fveq2 5679 . . . . . 6
2221fveq2d 5683 . . . . 5
2322cbvsumv 13157 . . . 4
2423oveq1i 6090 . . 3
251, 2, 3, 4, 20, 24ftalem1 22295 . 2
26 ftalem2.5 . . . . . 6
27 ftalem2.6 . . . . . . . . 9
28 plyf 21551 . . . . . . . . . . . . 13 Poly
293, 28syl 16 . . . . . . . . . . . 12
30 0cn 9366 . . . . . . . . . . . 12
31 ffvelrn 5829 . . . . . . . . . . . 12
3229, 30, 31sylancl 655 . . . . . . . . . . 11
3332abscld 12906 . . . . . . . . . 10
3433, 20rerpdivcld 11042 . . . . . . . . 9
3527, 34syl5eqel 2517 . . . . . . . 8
3635adantr 462 . . . . . . 7
37 simpr 458 . . . . . . . 8
38 1re 9373 . . . . . . . 8
39 ifcl 3819 . . . . . . . 8
4037, 38, 39sylancl 655 . . . . . . 7
41 ifcl 3819 . . . . . . 7
4236, 40, 41syl2anc 654 . . . . . 6
4326, 42syl5eqel 2517 . . . . 5
44 0red 9375 . . . . . 6
45 1red 9389 . . . . . 6
46 0lt1 9850 . . . . . . 7
4746a1i 11 . . . . . 6
48 max1 11145 . . . . . . . 8
4938, 37, 48sylancr 656 . . . . . . 7
50 max1 11145 . . . . . . . . 9
5140, 36, 50syl2anc 654 . . . . . . . 8
5251, 26syl6breqr 4320 . . . . . . 7
5345, 40, 43, 49, 52letrd 9516 . . . . . 6
5444, 45, 43, 47, 53ltletrd 9519 . . . . 5
5543, 54elrpd 11013 . . . 4
56 max2 11147 . . . . . . . . . . 11
5738, 37, 56sylancr 656 . . . . . . . . . 10
5837, 40, 43, 57, 52letrd 9516 . . . . . . . . 9
5958adantr 462 . . . . . . . 8
6037adantr 462 . . . . . . . . 9
6143adantr 462 . . . . . . . . 9
62 abscl 12751 . . . . . . . . . 10
6362adantl 463 . . . . . . . . 9
64 lelttr 9453 . . . . . . . . 9
6560, 61, 63, 64syl3anc 1211 . . . . . . . 8
6659, 65mpand 668 . . . . . . 7
6766imim1d 75 . . . . . 6
6829ad2antrr 718 . . . . . . . . . . . . . . 15
69 simprl 748 . . . . . . . . . . . . . . 15
7068, 69ffvelrnd 5832 . . . . . . . . . . . . . 14
718ad2antrr 718 . . . . . . . . . . . . . . 15
727ad2antrr 718 . . . . . . . . . . . . . . . 16
7369, 72expcld 11992 . . . . . . . . . . . . . . 15
7471, 73mulcld 9394 . . . . . . . . . . . . . 14
7570, 74subcld 9707 . . . . . . . . . . . . 13
7675abscld 12906 . . . . . . . . . . . 12
7774abscld 12906 . . . . . . . . . . . . 13
7877rehalfcld 10559 . . . . . . . . . . . 12
7976, 78, 77ltsub2d 9937 . . . . . . . . . . 11
8071, 73absmuld 12924 . . . . . . . . . . . . . . 15
8169, 72absexpd 12922 . . . . . . . . . . . . . . . 16
8281oveq2d 6096 . . . . . . . . . . . . . . 15
8380, 82eqtrd 2465 . . . . . . . . . . . . . 14
8483oveq1d 6095 . . . . . . . . . . . . 13
8571abscld 12906 . . . . . . . . . . . . . . 15
8685recnd 9400 . . . . . . . . . . . . . 14
8763adantrr 709 . . . . . . . . . . . . . . . 16
8887, 72reexpcld 12009 . . . . . . . . . . . . . . 15
8988recnd 9400 . . . . . . . . . . . . . 14
90 2cnd 10382 . . . . . . . . . . . . . 14
91 2ne0 10402 . . . . . . . . . . . . . . 15
9291a1i 11 . . . . . . . . . . . . . 14
9386, 89, 90, 92div23d 10132 . . . . . . . . . . . . 13
9484, 93eqtrd 2465 . . . . . . . . . . . 12
9594breq2d 4292 . . . . . . . . . . 11
9677recnd 9400 . . . . . . . . . . . . . . 15
97962halvesd 10558 . . . . . . . . . . . . . 14
9897oveq1d 6095 . . . . . . . . . . . . 13
9978recnd 9400 . . . . . . . . . . . . . 14
10099, 99pncand 9708 . . . . . . . . . . . . 13
10198, 100eqtr3d 2467 . . . . . . . . . . . 12
102101breq1d 4290 . . . . . . . . . . 11
10379, 95, 1023bitr3d 283 . . . . . . . . . 10
10474, 70subcld 9707 . . . . . . . . . . . . 13
10574, 104abs2difd 12927 . . . . . . . . . . . 12
10674, 70abssubd 12923 . . . . . . . . . . . . 13
107106oveq2d 6096 . . . . . . . . . . . 12
10874, 70nncand 9712 . . . . . . . . . . . . 13
109108fveq2d 5683 . . . . . . . . . . . 12
110105, 107, 1093brtr3d 4309 . . . . . . . . . . 11
11177, 76resubcld 9764 . . . . . . . . . . . 12
11270abscld 12906 . . . . . . . . . . . 12
113 ltletr 9454 . . . . . . . . . . . 12
11478, 111, 112, 113syl3anc 1211 . . . . . . . . . . 11
115110, 114mpan2d 667 . . . . . . . . . 10
116103, 115sylbid 215 . . . . . . . . 9
11733ad2antrr 718 . . . . . . . . . . . 12
11820ad2antrr 718 . . . . . . . . . . . . . 14
119118rpred 11015 . . . . . . . . . . . . 13
120119, 87remulcld 9402 . . . . . . . . . . . 12
12194, 78eqeltrrd 2508 . . . . . . . . . . . 12
12236adantr 462 . . . . . . . . . . . . . . 15
12343adantr 462 . . . . . . . . . . . . . . 15
124 max2 11147 . . . . . . . . . . . . . . . . . 18
12540, 36, 124syl2anc 654 . . . . . . . . . . . . . . . . 17
126125, 26syl6breqr 4320 . . . . . . . . . . . . . . . 16
127126adantr 462 . . . . . . . . . . . . . . 15
128 simprr 749 . . . . . . . . . . . . . . 15
129122, 123, 87, 127, 128lelttrd 9517 . . . . . . . . . . . . . 14
13027, 129syl5eqbrr 4314 . . . . . . . . . . . . 13
131117, 87, 118ltdivmuld 11062 . . . . . . . . . . . . 13
132130, 131mpbid 210 . . . . . . . . . . . 12
13387recnd 9400 . . . . . . . . . . . . . . 15
134133exp1d 11987 . . . . . . . . . . . . . 14
135 1red 9389 . . . . . . . . . . . . . . . 16
13653adantr 462 . . . . . . . . . . . . . . . . 17
137135, 123, 87, 136, 128lelttrd 9517 . . . . . . . . . . . . . . . 16
138135, 87, 137ltled 9510 . . . . . . . . . . . . . . 15
1394ad2antrr 718 . . . . . . . . . . . . . . . 16
140 nnuz 10884 . . . . . . . . . . . . . . . 16
141139, 140syl6eleq 2523 . . . . . . . . . . . . . . 15
14287, 138, 141leexp2ad 12024 . . . . . . . . . . . . . 14
143134, 142eqbrtrrd 4302 . . . . . . . . . . . . 13
14487, 88, 118lemul2d 11055 . . . . . . . . . . . . 13
145143, 144mpbid 210 . . . . . . . . . . . 12
146117, 120, 121, 132, 145ltletrd 9519 . . . . . . . . . . 11
147146, 94breqtrrd 4306 . . . . . . . . . 10
148 lttr 9439 . . . . . . . . . . 11
149117, 78, 112, 148syl3anc 1211 . . . . . . . . . 10
150147, 149mpand 668 . . . . . . . . 9
151116, 150syld 44 . . . . . . . 8
152151expr 610 . . . . . . 7
153152a2d 26 . . . . . 6
15467, 153syld 44 . . . . 5
155154ralimdva 2784 . . . 4
156 breq1 4283 . . . . . . 7
157156imbi1d 317 . . . . . 6
158157ralbidv 2725 . . . . 5
159158rspcev 3062 . . . 4
16055, 155, 159syl6an 540 . . 3
161160rexlimdva 2831 . 2
16225, 161mpd 15 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wceq 1362   wcel 1755   wne 2596  wral 2705  wrex 2706  cif 3779   class class class wbr 4280  wf 5402  cfv 5406  (class class class)co 6080  cc 9268  cr 9269  cc0 9270  c1 9271   caddc 9273   cmul 9275   clt 9406   cle 9407   cmin 9583   cdiv 9981  cn 10310  c2 10359  cn0 10567  cuz 10849  crp 10979  cfz 11424  cexp 11849  cabs 12707  csu 13147  c0p 20989  Polycply 21537  coeffccoe 21539  degcdgr 21540 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-inf2 7835  ax-cnex 9326  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-mulcom 9334  ax-addass 9335  ax-mulass 9336  ax-distr 9337  ax-i2m1 9338  ax-1ne0 9339  ax-1rid 9340  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343  ax-pre-lttri 9344  ax-pre-lttrn 9345  ax-pre-ltadd 9346  ax-pre-mulgt0 9347  ax-pre-sup 9348  ax-addf 9349 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-fal 1368  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-int 4117  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-se 4667  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-isom 5415  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-of 6309  df-om 6466  df-1st 6566  df-2nd 6567  df-recs 6818  df-rdg 6852  df-1o 6908  df-oadd 6912  df-er 7089  df-map 7204  df-pm 7205  df-en 7299  df-dom 7300  df-sdom 7301  df-fin 7302  df-sup 7679  df-oi 7712  df-card 8097  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412  df-sub 9585  df-neg 9586  df-div 9982  df-nn 10311  df-2 10368  df-3 10369  df-n0 10568  df-z 10635  df-uz 10850  df-rp 10980  df-ico 11294  df-fz 11425  df-fzo 11533  df-fl 11626  df-seq 11791  df-exp 11850  df-hash 12088  df-cj 12572  df-re 12573  df-im 12574  df-sqr 12708  df-abs 12709  df-clim 12950  df-rlim 12951  df-sum 13148  df-0p 20990  df-ply 21541  df-coe 21543  df-dgr 21544 This theorem is referenced by:  fta  22302
 Copyright terms: Public domain W3C validator