Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  signsplypnf Structured version   Unicode version

Theorem signsplypnf 28147
 Description: The quotient of a polynomial by a monic monomial of same degree converges to the highest coefficient of . (Contributed by Thierry Arnoux, 18-Sep-2018.)
Hypotheses
Ref Expression
signsply0.d deg
signsply0.c coeff
signsply0.b
signsplypnf.g
Assertion
Ref Expression
signsplypnf Poly
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem signsplypnf
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 sumex 13469 . . . . 5 ..^
21a1i 11 . . . 4 Poly ..^
3 sumex 13469 . . . . 5
43a1i 11 . . . 4 Poly
5 rpssre 11226 . . . . . . 7
65a1i 11 . . . . . 6 Poly
7 fzofi 12048 . . . . . . 7 ..^
87a1i 11 . . . . . 6 Poly ..^
9 ovex 6307 . . . . . . 7
109a1i 11 . . . . . 6 Poly ..^
11 fvex 5874 . . . . . . . . . 10
1211a1i 11 . . . . . . . . 9 Poly ..^
13 ovex 6307 . . . . . . . . . 10
1413a1i 11 . . . . . . . . 9 Poly ..^
15 signsply0.c . . . . . . . . . . . . 13 coeff
1615coef3 22364 . . . . . . . . . . . 12 Poly
1716adantr 465 . . . . . . . . . . 11 Poly ..^
18 elfzouz 11797 . . . . . . . . . . . . 13 ..^
19 nn0uz 11112 . . . . . . . . . . . . 13
2018, 19syl6eleqr 2566 . . . . . . . . . . . 12 ..^
2120adantl 466 . . . . . . . . . . 11 Poly ..^
2217, 21ffvelrnd 6020 . . . . . . . . . 10 Poly ..^
23 rlimconst 13326 . . . . . . . . . 10
245, 22, 23sylancr 663 . . . . . . . . 9 Poly ..^
2521nn0red 10849 . . . . . . . . . . . 12 Poly ..^
26 signsply0.d . . . . . . . . . . . . . . 15 deg
27 dgrcl 22365 . . . . . . . . . . . . . . 15 Poly deg
2826, 27syl5eqel 2559 . . . . . . . . . . . . . 14 Poly
2928adantr 465 . . . . . . . . . . . . 13 Poly ..^
3029nn0red 10849 . . . . . . . . . . . 12 Poly ..^
31 elfzolt2 11801 . . . . . . . . . . . . 13 ..^
3231adantl 466 . . . . . . . . . . . 12 Poly ..^
33 difrp 11249 . . . . . . . . . . . . 13
3433biimpa 484 . . . . . . . . . . . 12
3525, 30, 32, 34syl21anc 1227 . . . . . . . . . . 11 Poly ..^
36 cxplim 23029 . . . . . . . . . . 11
3735, 36syl 16 . . . . . . . . . 10 Poly ..^
38 ax-resscn 9545 . . . . . . . . . . . . . . . . . . . 20
395, 38sstri 3513 . . . . . . . . . . . . . . . . . . 19
4039a1i 11 . . . . . . . . . . . . . . . . . 18 Poly
4140sselda 3504 . . . . . . . . . . . . . . . . 17 Poly
4241adantlr 714 . . . . . . . . . . . . . . . 16 Poly ..^
43 rpgt0 11227 . . . . . . . . . . . . . . . . . 18
4443gt0ne0d 10113 . . . . . . . . . . . . . . . . 17
4544adantl 466 . . . . . . . . . . . . . . . 16 Poly ..^
4628nn0zd 10960 . . . . . . . . . . . . . . . . . . 19 Poly
4746adantr 465 . . . . . . . . . . . . . . . . . 18 Poly
4847adantlr 714 . . . . . . . . . . . . . . . . 17 Poly ..^
4920ad2antlr 726 . . . . . . . . . . . . . . . . . 18 Poly ..^
5049nn0zd 10960 . . . . . . . . . . . . . . . . 17 Poly ..^
5148, 50zsubcld 10967 . . . . . . . . . . . . . . . 16 Poly ..^
5242, 45, 51cxpexpzd 22820 . . . . . . . . . . . . . . 15 Poly ..^
5352oveq2d 6298 . . . . . . . . . . . . . 14 Poly ..^
5442, 45, 51expnegd 12281 . . . . . . . . . . . . . 14 Poly ..^
5548zcnd 10963 . . . . . . . . . . . . . . . 16 Poly ..^
5649nn0cnd 10850 . . . . . . . . . . . . . . . 16 Poly ..^
5755, 56negsubdi2d 9942 . . . . . . . . . . . . . . 15 Poly ..^
5857oveq2d 6298 . . . . . . . . . . . . . 14 Poly ..^
5953, 54, 583eqtr2d 2514 . . . . . . . . . . . . 13 Poly ..^
6042, 45, 48, 50expsubd 12285 . . . . . . . . . . . . 13 Poly ..^
6159, 60eqtrd 2508 . . . . . . . . . . . 12 Poly ..^
6261mpteq2dva 4533 . . . . . . . . . . 11 Poly ..^
6362breq1d 4457 . . . . . . . . . 10 Poly ..^
6437, 63mpbid 210 . . . . . . . . 9 Poly ..^
6512, 14, 24, 64rlimmul 13426 . . . . . . . 8 Poly ..^
6622mul01d 9774 . . . . . . . 8 Poly ..^
6765, 66breqtrd 4471 . . . . . . 7 Poly ..^
6816ad2antrr 725 . . . . . . . . . . 11 Poly ..^
6968, 49ffvelrnd 6020 . . . . . . . . . 10 Poly ..^
7042, 49expcld 12274 . . . . . . . . . 10 Poly ..^
7128adantr 465 . . . . . . . . . . . 12 Poly
7241, 71expcld 12274 . . . . . . . . . . 11 Poly
7372adantlr 714 . . . . . . . . . 10 Poly ..^
7442, 45, 48expne0d 12280 . . . . . . . . . 10 Poly ..^
7569, 70, 73, 74divassd 10351 . . . . . . . . 9 Poly ..^
7675mpteq2dva 4533 . . . . . . . 8 Poly ..^
7776breq1d 4457 . . . . . . 7 Poly ..^
7867, 77mpbird 232 . . . . . 6 Poly ..^
796, 8, 10, 78fsumrlim 13584 . . . . 5 Poly ..^ ..^
808olcd 393 . . . . . 6 Poly ..^ ..^
81 sumz 13503 . . . . . 6 ..^ ..^ ..^
8280, 81syl 16 . . . . 5 Poly ..^
8379, 82breqtrd 4471 . . . 4 Poly ..^
8416, 28ffvelrnd 6020 . . . . . . . . . . 11 Poly
8584adantr 465 . . . . . . . . . 10 Poly
8685, 72mulcld 9612 . . . . . . . . 9 Poly
8744adantl 466 . . . . . . . . . 10 Poly
8841, 87, 47expne0d 12280 . . . . . . . . 9 Poly
8986, 72, 88divcld 10316 . . . . . . . 8 Poly
90 fveq2 5864 . . . . . . . . . . 11
91 oveq2 6290 . . . . . . . . . . 11
9290, 91oveq12d 6300 . . . . . . . . . 10
9392oveq1d 6297 . . . . . . . . 9
9493sumsn 13522 . . . . . . . 8
9571, 89, 94syl2anc 661 . . . . . . 7 Poly
96 divcan4 10228 . . . . . . . 8
9785, 72, 88, 96syl3anc 1228 . . . . . . 7 Poly
9895, 97eqtrd 2508 . . . . . 6 Poly
9998mpteq2dva 4533 . . . . 5 Poly
100 rlimconst 13326 . . . . . 6
1016, 84, 100syl2anc 661 . . . . 5 Poly
10299, 101eqbrtrd 4467 . . . 4 Poly
1032, 4, 83, 102rlimadd 13424 . . 3 Poly ..^
10484addid2d 9776 . . . 4 Poly
105 signsply0.b . . . 4
106104, 105syl6eqr 2526 . . 3 Poly
107103, 106breqtrd 4471 . 2 Poly ..^
108 plyf 22330 . . . . . 6 Poly
109 ffn 5729 . . . . . 6
110108, 109syl 16 . . . . 5 Poly
111 ovex 6307 . . . . . . 7
112111rgenw 2825 . . . . . 6
113 signsplypnf.g . . . . . . 7
114113fnmpt 5705 . . . . . 6
115112, 114mp1i 12 . . . . 5 Poly
116 cnex 9569 . . . . . 6
117116a1i 11 . . . . 5 Poly
118 reex 9579 . . . . . . 7
119118, 5ssexi 4592 . . . . . 6
120119a1i 11 . . . . 5 Poly
121 dfss1 3703 . . . . . 6
12239, 121mpbi 208 . . . . 5
12315, 26coeid2 22371 . . . . 5 Poly
124113fvmpt2 5955 . . . . . . 7
125111, 124mpan2 671 . . . . . 6
126125adantl 466 . . . . 5 Poly
127110, 115, 117, 120, 122, 123, 126offval 6529 . . . 4 Poly
128 fzfid 12047 . . . . . . 7 Poly
12916ad2antrr 725 . . . . . . . . 9 Poly
130 elfznn0 11766 . . . . . . . . . 10
131130adantl 466 . . . . . . . . 9 Poly
132129, 131ffvelrnd 6020 . . . . . . . 8 Poly
13341adantr 465 . . . . . . . . 9 Poly
134133, 131expcld 12274 . . . . . . . 8 Poly
135132, 134mulcld 9612 . . . . . . 7 Poly
136128, 72, 135, 88fsumdivc 13560 . . . . . 6 Poly
137 fzodisj 11823 . . . . . . . . 9 ..^ ..^
138 fzosn 11850 . . . . . . . . . 10 ..^
139138ineq2d 3700 . . . . . . . . 9 ..^ ..^ ..^
140137, 139syl5reqr 2523 . . . . . . . 8 ..^
14147, 140syl 16 . . . . . . 7 Poly ..^
142 fzval3 11849 . . . . . . . . . 10 ..^
14346, 142syl 16 . . . . . . . . 9 Poly ..^
14428, 19syl6eleq 2565 . . . . . . . . . 10 Poly
145 fzosplitsn 11882 . . . . . . . . . 10 ..^ ..^
146144, 145syl 16 . . . . . . . . 9 Poly ..^ ..^
147143, 146eqtrd 2508 . . . . . . . 8 Poly ..^
148147adantr 465 . . . . . . 7 Poly ..^
14972adantr 465 . . . . . . . 8 Poly
15087adantr 465 . . . . . . . . 9 Poly
15147adantr 465 . . . . . . . . 9 Poly
152133, 150, 151expne0d 12280 . . . . . . . 8 Poly
153135, 149, 152divcld 10316 . . . . . . 7 Poly
154141, 148, 128, 153fsumsplit 13521 . . . . . 6 Poly ..^
155136, 154eqtrd 2508 . . . . 5 Poly ..^
156155mpteq2dva 4533 . . . 4 Poly ..^
157127, 156eqtrd 2508 . . 3 Poly ..^
158157breq1d 4457 . 2 Poly ..^
159107, 158mpbird 232 1 Poly
 Colors of variables: wff setvar class Syntax hints:   wi 4   wo 368   wa 369   wceq 1379   wcel 1767   wne 2662  wral 2814  cvv 3113   cun 3474   cin 3475   wss 3476  c0 3785  csn 4027   class class class wbr 4447   cmpt 4505   wfn 5581  wf 5582  cfv 5586  (class class class)co 6282   cof 6520  cfn 7513  cc 9486  cr 9487  cc0 9488  c1 9489   caddc 9491   cmul 9493   clt 9624   cmin 9801  cneg 9802   cdiv 10202  cn0 10791  cz 10860  cuz 11078  crp 11216  cfz 11668  ..^cfzo 11788  cexp 12130   crli 13267  csu 13467  Polycply 22316  coeffccoe 22318  degcdgr 22319   ccxp 22671 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-inf2 8054  ax-cnex 9544  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564  ax-pre-mulgt0 9565  ax-pre-sup 9566  ax-addf 9567  ax-mulf 9568 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-iin 4328  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-isom 5595  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-of 6522  df-om 6679  df-1st 6781  df-2nd 6782  df-supp 6899  df-recs 7039  df-rdg 7073  df-1o 7127  df-2o 7128  df-oadd 7131  df-er 7308  df-map 7419  df-pm 7420  df-ixp 7467  df-en 7514  df-dom 7515  df-sdom 7516  df-fin 7517  df-fsupp 7826  df-fi 7867  df-sup 7897  df-oi 7931  df-card 8316  df-cda 8544  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-sub 9803  df-neg 9804  df-div 10203  df-nn 10533  df-2 10590  df-3 10591  df-4 10592  df-5 10593  df-6 10594  df-7 10595  df-8 10596  df-9 10597  df-10 10598  df-n0 10792  df-z 10861  df-dec 10973  df-uz 11079  df-q 11179  df-rp 11217  df-xneg 11314  df-xadd 11315  df-xmul 11316  df-ioo 11529  df-ioc 11530  df-ico 11531  df-icc 11532  df-fz 11669  df-fzo 11789  df-fl 11893  df-mod 11961  df-seq 12072  df-exp 12131  df-fac 12318  df-bc 12345  df-hash 12370  df-shft 12859  df-cj 12891  df-re 12892  df-im 12893  df-sqrt 13027  df-abs 13028  df-limsup 13253  df-clim 13270  df-rlim 13271  df-sum 13468  df-ef 13661  df-sin 13663  df-cos 13664  df-pi 13666  df-struct 14488  df-ndx 14489  df-slot 14490  df-base 14491  df-sets 14492  df-ress 14493  df-plusg 14564  df-mulr 14565  df-starv 14566  df-sca 14567  df-vsca 14568  df-ip 14569  df-tset 14570  df-ple 14571  df-ds 14573  df-unif 14574  df-hom 14575  df-cco 14576  df-rest 14674  df-topn 14675  df-0g 14693  df-gsum 14694  df-topgen 14695  df-pt 14696  df-prds 14699  df-xrs 14753  df-qtop 14758  df-imas 14759  df-xps 14761  df-mre 14837  df-mrc 14838  df-acs 14840  df-mnd 15728  df-submnd 15778  df-mulg 15861  df-cntz 16150  df-cmn 16596  df-psmet 18182  df-xmet 18183  df-met 18184  df-bl 18185  df-mopn 18186  df-fbas 18187  df-fg 18188  df-cnfld 18192  df-top 19166  df-bases 19168  df-topon 19169  df-topsp 19170  df-cld 19286  df-ntr 19287  df-cls 19288  df-nei 19365  df-lp 19403  df-perf 19404  df-cn 19494  df-cnp 19495  df-haus 19582  df-tx 19798  df-hmeo 19991  df-fil 20082  df-fm 20174  df-flim 20175  df-flf 20176  df-xms 20558  df-ms 20559  df-tms 20560  df-cncf 21117  df-0p 21812  df-limc 22005  df-dv 22006  df-ply 22320  df-coe 22322  df-dgr 22323  df-log 22672  df-cxp 22673 This theorem is referenced by:  signsply0  28148
 Copyright terms: Public domain W3C validator