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

Theorem plydivex 20215
 Description: Lemma for plydivalg 20217. (Contributed by Mario Carneiro, 24-Jul-2014.)
Hypotheses
Ref Expression
plydiv.pl
plydiv.tm
plydiv.rc
plydiv.m1
plydiv.f Poly
plydiv.g Poly
plydiv.z
plydiv.r
Assertion
Ref Expression
plydivex Poly deg deg
Distinct variable groups:   ,,,   ,,   ,,,   ,,   ,,,
Allowed substitution hints:   ()   ()

Proof of Theorem plydivex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 plydiv.f . . . . . 6 Poly
2 dgrcl 20153 . . . . . 6 Poly deg
31, 2syl 16 . . . . 5 deg
43nn0red 10276 . . . 4 deg
5 plydiv.g . . . . . 6 Poly
6 dgrcl 20153 . . . . . 6 Poly deg
75, 6syl 16 . . . . 5 deg
87nn0red 10276 . . . 4 deg
94, 8resubcld 9466 . . 3 deg deg
10 arch 10219 . . 3 deg deg deg deg
119, 10syl 16 . 2 deg deg
12 olc 375 . . . 4 deg deg deg deg
131adantr 453 . . . . 5 Poly
14 nnnn0 10229 . . . . . . 7
15 breq2 4217 . . . . . . . . . . . 12 deg deg deg deg
1615orbi2d 684 . . . . . . . . . . 11 deg deg deg deg
1716imbi1d 310 . . . . . . . . . 10 deg deg Poly deg deg deg deg Poly deg deg
1817ralbidv 2726 . . . . . . . . 9 Poly deg deg Poly deg deg Poly deg deg Poly deg deg
1918imbi2d 309 . . . . . . . 8 Poly deg deg Poly deg deg Poly deg deg Poly deg deg
20 breq2 4217 . . . . . . . . . . . 12 deg deg deg deg
2120orbi2d 684 . . . . . . . . . . 11 deg deg deg deg
2221imbi1d 310 . . . . . . . . . 10 deg deg Poly deg deg deg deg Poly deg deg
2322ralbidv 2726 . . . . . . . . 9 Poly deg deg Poly deg deg Poly deg deg Poly deg deg
2423imbi2d 309 . . . . . . . 8 Poly deg deg Poly deg deg Poly deg deg Poly deg deg
25 breq2 4217 . . . . . . . . . . . 12 deg deg deg deg
2625orbi2d 684 . . . . . . . . . . 11 deg deg deg deg
2726imbi1d 310 . . . . . . . . . 10 deg deg Poly deg deg deg deg Poly deg deg
2827ralbidv 2726 . . . . . . . . 9 Poly deg deg Poly deg deg Poly deg deg Poly deg deg
2928imbi2d 309 . . . . . . . 8 Poly deg deg Poly deg deg Poly deg deg Poly deg deg
30 plydiv.pl . . . . . . . . . . . 12
3130adantlr 697 . . . . . . . . . . 11 Poly deg deg
32 plydiv.tm . . . . . . . . . . . 12
3332adantlr 697 . . . . . . . . . . 11 Poly deg deg
34 plydiv.rc . . . . . . . . . . . 12
3534adantlr 697 . . . . . . . . . . 11 Poly deg deg
36 plydiv.m1 . . . . . . . . . . . 12
3736adantr 453 . . . . . . . . . . 11 Poly deg deg
38 simprl 734 . . . . . . . . . . 11 Poly deg deg Poly
395adantr 453 . . . . . . . . . . 11 Poly deg deg Poly
40 plydiv.z . . . . . . . . . . . 12
4140adantr 453 . . . . . . . . . . 11 Poly deg deg
42 eqid 2437 . . . . . . . . . . 11
43 simprr 735 . . . . . . . . . . 11 Poly deg deg deg deg
4431, 33, 35, 37, 38, 39, 41, 42, 43plydivlem3 20213 . . . . . . . . . 10 Poly deg deg Poly deg deg
4544expr 600 . . . . . . . . 9 Poly deg deg Poly deg deg
4645ralrimiva 2790 . . . . . . . 8 Poly deg deg Poly deg deg
47 eqeq1 2443 . . . . . . . . . . . . . . . 16
48 fveq2 5729 . . . . . . . . . . . . . . . . . 18 deg deg
4948oveq1d 6097 . . . . . . . . . . . . . . . . 17 deg deg deg deg
5049breq1d 4223 . . . . . . . . . . . . . . . 16 deg deg deg deg
5147, 50orbi12d 692 . . . . . . . . . . . . . . 15 deg deg deg deg
52 oveq1 6089 . . . . . . . . . . . . . . . . . 18
5352eqeq1d 2445 . . . . . . . . . . . . . . . . 17
5452fveq2d 5733 . . . . . . . . . . . . . . . . . 18 deg deg
5554breq1d 4223 . . . . . . . . . . . . . . . . 17 deg deg deg deg
5653, 55orbi12d 692 . . . . . . . . . . . . . . . 16 deg deg deg deg
5756rexbidv 2727 . . . . . . . . . . . . . . 15 Poly deg deg Poly deg deg
5851, 57imbi12d 313 . . . . . . . . . . . . . 14 deg deg Poly deg deg deg deg Poly deg deg
5958cbvralv 2933 . . . . . . . . . . . . 13 Poly deg deg Poly deg deg Poly deg deg Poly deg deg
60 simplll 736 . . . . . . . . . . . . . . . . 17 Poly Poly deg deg Poly deg deg deg deg
6160, 30sylan 459 . . . . . . . . . . . . . . . 16 Poly Poly deg deg Poly deg deg deg deg
6260, 32sylan 459 . . . . . . . . . . . . . . . 16 Poly Poly deg deg Poly deg deg deg deg
6360, 34sylan 459 . . . . . . . . . . . . . . . 16 Poly Poly deg deg Poly deg deg deg deg
6460, 36syl 16 . . . . . . . . . . . . . . . 16 Poly Poly deg deg Poly deg deg deg deg
65 simplr 733 . . . . . . . . . . . . . . . 16 Poly Poly deg deg Poly deg deg deg deg Poly
6660, 5syl 16 . . . . . . . . . . . . . . . 16 Poly Poly deg deg Poly deg deg deg deg Poly
6760, 40syl 16 . . . . . . . . . . . . . . . 16 Poly Poly deg deg Poly deg deg deg deg
68 simpllr 737 . . . . . . . . . . . . . . . 16 Poly Poly deg deg Poly deg deg deg deg
69 simprrr 743 . . . . . . . . . . . . . . . 16 Poly Poly deg deg Poly deg deg deg deg deg deg
70 simprrl 742 . . . . . . . . . . . . . . . 16 Poly Poly deg deg Poly deg deg deg deg
71 eqid 2437 . . . . . . . . . . . . . . . 16
72 oveq1 6089 . . . . . . . . . . . . . . . . . 18
7372oveq2d 6098 . . . . . . . . . . . . . . . . 17 coeffdeg coeffdeg coeffdeg coeffdeg
7473cbvmptv 4301 . . . . . . . . . . . . . . . 16 coeffdeg coeffdeg coeffdeg coeffdeg
75 simprl 734 . . . . . . . . . . . . . . . . 17 Poly Poly deg deg Poly deg deg deg deg Poly deg deg Poly deg deg
76 oveq2 6090 . . . . . . . . . . . . . . . . . . . . . . 23
7776oveq2d 6098 . . . . . . . . . . . . . . . . . . . . . 22
7877eqeq1d 2445 . . . . . . . . . . . . . . . . . . . . 21
7977fveq2d 5733 . . . . . . . . . . . . . . . . . . . . . 22 deg deg
8079breq1d 4223 . . . . . . . . . . . . . . . . . . . . 21 deg deg deg deg
8178, 80orbi12d 692 . . . . . . . . . . . . . . . . . . . 20 deg deg deg deg
8281cbvrexv 2934 . . . . . . . . . . . . . . . . . . 19 Poly deg deg Poly deg deg
8382imbi2i 305 . . . . . . . . . . . . . . . . . 18 deg deg Poly deg deg deg deg Poly deg deg
8483ralbii 2730 . . . . . . . . . . . . . . . . 17 Poly deg deg Poly deg deg Poly deg deg Poly deg deg
8575, 84sylib 190 . . . . . . . . . . . . . . . 16 Poly Poly deg deg Poly deg deg deg deg Poly deg deg Poly deg deg
86 eqid 2437 . . . . . . . . . . . . . . . 16 coeff coeff
87 eqid 2437 . . . . . . . . . . . . . . . 16 coeff coeff
88 eqid 2437 . . . . . . . . . . . . . . . 16 deg deg
89 eqid 2437 . . . . . . . . . . . . . . . 16 deg deg
9061, 62, 63, 64, 65, 66, 67, 42, 68, 69, 70, 71, 74, 85, 86, 87, 88, 89plydivlem4 20214 . . . . . . . . . . . . . . 15 Poly Poly deg deg Poly deg deg deg deg Poly deg deg
9190exp32 590 . . . . . . . . . . . . . 14 Poly Poly deg deg Poly deg deg deg deg Poly deg deg
9291ralrimdva 2797 . . . . . . . . . . . . 13 Poly deg deg Poly deg deg Poly deg deg Poly deg deg
9359, 92syl5bi 210 . . . . . . . . . . . 12 Poly deg deg Poly deg deg Poly deg deg Poly deg deg
9493ancld 538 . . . . . . . . . . 11 Poly deg deg Poly deg deg Poly deg deg Poly deg deg Poly deg deg Poly deg deg
95 dgrcl 20153 . . . . . . . . . . . . . . . . . . . . . 22 Poly deg
9695adantl 454 . . . . . . . . . . . . . . . . . . . . 21 Poly deg
9796nn0zd 10374 . . . . . . . . . . . . . . . . . . . 20 Poly deg
985ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . 22 Poly Poly
9998, 6syl 16 . . . . . . . . . . . . . . . . . . . . 21 Poly deg
10099nn0zd 10374 . . . . . . . . . . . . . . . . . . . 20 Poly deg
10197, 100zsubcld 10381 . . . . . . . . . . . . . . . . . . 19 Poly deg deg
102 nn0z 10305 . . . . . . . . . . . . . . . . . . . 20
103102ad2antlr 709 . . . . . . . . . . . . . . . . . . 19 Poly
104 zleltp1 10327 . . . . . . . . . . . . . . . . . . 19 deg deg deg deg deg deg
105101, 103, 104syl2anc 644 . . . . . . . . . . . . . . . . . 18 Poly deg deg deg deg
106101zred 10376 . . . . . . . . . . . . . . . . . . 19 Poly deg deg
107 nn0re 10231 . . . . . . . . . . . . . . . . . . . 20
108107ad2antlr 709 . . . . . . . . . . . . . . . . . . 19 Poly
109106, 108leloed 9217 . . . . . . . . . . . . . . . . . 18 Poly deg deg deg deg deg deg
110105, 109bitr3d 248 . . . . . . . . . . . . . . . . 17 Poly deg deg deg deg deg deg
111110orbi2d 684 . . . . . . . . . . . . . . . 16 Poly deg deg deg deg deg deg
112 pm5.63 892 . . . . . . . . . . . . . . . . . . . 20 deg deg deg deg
113 df-ne 2602 . . . . . . . . . . . . . . . . . . . . . 22
114113anbi1i 678 . . . . . . . . . . . . . . . . . . . . 21 deg deg deg deg
115114orbi2i 507 . . . . . . . . . . . . . . . . . . . 20 deg deg deg deg
116112, 115bitr4i 245 . . . . . . . . . . . . . . . . . . 19 deg deg deg deg
117116orbi2i 507 . . . . . . . . . . . . . . . . . 18 deg deg deg deg deg deg deg deg
118 or12 511 . . . . . . . . . . . . . . . . . 18 deg deg deg deg deg deg deg deg
119 or12 511 . . . . . . . . . . . . . . . . . 18 deg deg deg deg deg deg deg deg
120117, 118, 1193bitr4i 270 . . . . . . . . . . . . . . . . 17 deg deg deg deg deg deg deg deg
121 orass 512 . . . . . . . . . . . . . . . . 17 deg deg deg deg deg deg deg deg
122120, 121bitr4i 245 . . . . . . . . . . . . . . . 16 deg deg deg deg deg deg deg deg
123111, 122syl6bb 254 . . . . . . . . . . . . . . 15 Poly deg deg deg deg deg deg
124123imbi1d 310 . . . . . . . . . . . . . 14 Poly deg deg Poly deg deg deg deg deg deg Poly deg deg
125 jaob 760 . . . . . . . . . . . . . 14 deg deg deg deg Poly deg deg deg deg Poly deg deg deg deg Poly deg deg
126124, 125syl6bb 254 . . . . . . . . . . . . 13 Poly deg deg Poly deg deg deg deg Poly deg deg deg deg Poly deg deg
127126ralbidva 2722 . . . . . . . . . . . 12 Poly deg deg Poly deg deg Poly deg deg Poly deg deg deg deg Poly deg deg
128 r19.26 2839 . . . . . . . . . . . 12 Poly deg deg Poly deg deg deg deg Poly deg deg Poly deg deg Poly deg deg Poly deg deg Poly deg deg
129127, 128syl6bb 254 . . . . . . . . . . 11 Poly deg deg Poly deg deg Poly deg deg Poly deg deg Poly deg deg Poly deg deg
13094, 129sylibrd 227 . . . . . . . . . 10 Poly deg deg Poly deg deg Poly deg deg Poly deg deg
131130expcom 426 . . . . . . . . 9 Poly deg deg Poly deg deg Poly deg deg Poly deg deg
132131a2d 25 . . . . . . . 8 Poly deg deg Poly deg deg Poly deg deg Poly deg deg
13319, 24, 29, 24, 46, 132nn0ind 10367 . . . . . . 7 Poly deg deg Poly deg deg
13414, 133syl 16 . . . . . 6 Poly deg deg Poly deg deg
135134impcom 421 . . . . 5 Poly deg deg Poly deg deg
136 eqeq1 2443 . . . . . . . 8
137 fveq2 5729 . . . . . . . . . 10 deg deg
138137oveq1d 6097 . . . . . . . . 9 deg deg deg deg
139138breq1d 4223 . . . . . . . 8 deg deg deg deg
140136, 139orbi12d 692 . . . . . . 7 deg deg deg deg
141 oveq1 6089 . . . . . . . . . . 11
142 plydiv.r . . . . . . . . . . 11
143141, 142syl6eqr 2487 . . . . . . . . . 10
144143eqeq1d 2445 . . . . . . . . 9
145143fveq2d 5733 . . . . . . . . . 10 deg deg
146145breq1d 4223 . . . . . . . . 9 deg deg deg deg
147144, 146orbi12d 692 . . . . . . . 8 deg deg deg deg
148147rexbidv 2727 . . . . . . 7 Poly deg deg Poly deg deg
149140, 148imbi12d 313 . . . . . 6 deg deg Poly deg deg deg deg Poly deg deg
150149rspcv 3049 . . . . 5 Poly Poly deg deg Poly deg deg deg deg Poly deg deg
15113, 135, 150sylc 59 . . . 4 deg deg Poly deg deg
15212, 151syl5 31 . . 3 deg deg Poly deg deg
153152rexlimdva 2831 . 2 deg deg Poly deg deg
15411, 153mpd 15 1 Poly deg deg
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wo 359   wa 360   wceq 1653   wcel 1726   wne 2600  wral 2706  wrex 2707   class class class wbr 4213   cmpt 4267  cfv 5455  (class class class)co 6082   cof 6304  cc 8989  cr 8990  cc0 8991  c1 8992   caddc 8994   cmul 8996   clt 9121   cle 9122   cmin 9292  cneg 9293   cdiv 9678  cn 10001  cn0 10222  cz 10283  cexp 11383  c0p 19562  Polycply 20104  coeffccoe 20106  degcdgr 20107 This theorem is referenced by:  plydivalg  20217 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-rep 4321  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702  ax-inf2 7597  ax-cnex 9047  ax-resscn 9048  ax-1cn 9049  ax-icn 9050  ax-addcl 9051  ax-addrcl 9052  ax-mulcl 9053  ax-mulrcl 9054  ax-mulcom 9055  ax-addass 9056  ax-mulass 9057  ax-distr 9058  ax-i2m1 9059  ax-1ne0 9060  ax-1rid 9061  ax-rnegex 9062  ax-rrecex 9063  ax-cnre 9064  ax-pre-lttri 9065  ax-pre-lttrn 9066  ax-pre-ltadd 9067  ax-pre-mulgt0 9068  ax-pre-sup 9069  ax-addf 9070 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2711  df-rex 2712  df-reu 2713  df-rmo 2714  df-rab 2715  df-v 2959  df-sbc 3163  df-csb 3253  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-tp 3823  df-op 3824  df-uni 4017  df-int 4052  df-iun 4096  df-br 4214  df-opab 4268  df-mpt 4269  df-tr 4304  df-eprel 4495  df-id 4499  df-po 4504  df-so 4505  df-fr 4542  df-se 4543  df-we 4544  df-ord 4585  df-on 4586  df-lim 4587  df-suc 4588  df-om 4847  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-isom 5464  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-of 6306  df-1st 6350  df-2nd 6351  df-riota 6550  df-recs 6634  df-rdg 6669  df-1o 6725  df-oadd 6729  df-er 6906  df-map 7021  df-pm 7022  df-en 7111  df-dom 7112  df-sdom 7113  df-fin 7114  df-sup 7447  df-oi 7480  df-card 7827  df-pnf 9123  df-mnf 9124  df-xr 9125  df-ltxr 9126  df-le 9127  df-sub 9294  df-neg 9295  df-div 9679  df-nn 10002  df-2 10059  df-3 10060  df-n0 10223  df-z 10284  df-uz 10490  df-rp 10614  df-fz 11045  df-fzo 11137  df-fl 11203  df-seq 11325  df-exp 11384  df-hash 11620  df-cj 11905  df-re 11906  df-im 11907  df-sqr 12041  df-abs 12042  df-clim 12283  df-rlim 12284  df-sum 12481  df-0p 19563  df-ply 20108  df-coe 20110  df-dgr 20111
 Copyright terms: Public domain W3C validator