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

Theorem plydiveu 20168
 Description: Lemma for plydivalg 20169. (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
plydiveu.q Poly
plydiveu.qd deg deg
plydiveu.t
plydiveu.p Poly
plydiveu.pd deg deg
Assertion
Ref Expression
plydiveu
Distinct variable groups:   ,   ,,,,   ,,   ,,   ,,,,   ,,,   ,,,,
Allowed substitution hints:   (,)   ()   (,)

Proof of Theorem plydiveu
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 idd 22 . . . 4
2 plydiveu.q . . . . . . . . . . . . . . . 16 Poly
3 plydiv.pl . . . . . . . . . . . . . . . . 17
4 plydiv.tm . . . . . . . . . . . . . . . . 17
5 plydiv.rc . . . . . . . . . . . . . . . . 17
6 plydiv.m1 . . . . . . . . . . . . . . . . 17
7 plydiv.f . . . . . . . . . . . . . . . . 17 Poly
8 plydiv.g . . . . . . . . . . . . . . . . 17 Poly
9 plydiv.z . . . . . . . . . . . . . . . . 17
10 plydiv.r . . . . . . . . . . . . . . . . 17
113, 4, 5, 6, 7, 8, 9, 10plydivlem2 20164 . . . . . . . . . . . . . . . 16 Poly Poly
122, 11mpdan 650 . . . . . . . . . . . . . . 15 Poly
13 plydiveu.p . . . . . . . . . . . . . . . 16 Poly
14 plydiveu.t . . . . . . . . . . . . . . . . 17
153, 4, 5, 6, 7, 8, 9, 14plydivlem2 20164 . . . . . . . . . . . . . . . 16 Poly Poly
1613, 15mpdan 650 . . . . . . . . . . . . . . 15 Poly
1712, 16, 3, 4, 6plysub 20091 . . . . . . . . . . . . . 14 Poly
18 dgrcl 20105 . . . . . . . . . . . . . 14 Poly deg
1917, 18syl 16 . . . . . . . . . . . . 13 deg
2019nn0red 10231 . . . . . . . . . . . 12 deg
21 dgrcl 20105 . . . . . . . . . . . . . . 15 Poly deg
2216, 21syl 16 . . . . . . . . . . . . . 14 deg
2322nn0red 10231 . . . . . . . . . . . . 13 deg
24 dgrcl 20105 . . . . . . . . . . . . . . 15 Poly deg
2512, 24syl 16 . . . . . . . . . . . . . 14 deg
2625nn0red 10231 . . . . . . . . . . . . 13 deg
27 ifcl 3735 . . . . . . . . . . . . 13 deg deg deg deg deg deg
2823, 26, 27syl2anc 643 . . . . . . . . . . . 12 deg deg deg deg
29 dgrcl 20105 . . . . . . . . . . . . . 14 Poly deg
308, 29syl 16 . . . . . . . . . . . . 13 deg
3130nn0red 10231 . . . . . . . . . . . 12 deg
32 eqid 2404 . . . . . . . . . . . . . 14 deg deg
33 eqid 2404 . . . . . . . . . . . . . 14 deg deg
3432, 33dgrsub 20143 . . . . . . . . . . . . 13 Poly Poly deg deg deg deg deg
3512, 16, 34syl2anc 643 . . . . . . . . . . . 12 deg deg deg deg deg
36 plydiveu.pd . . . . . . . . . . . . . . 15 deg deg
37 eqid 2404 . . . . . . . . . . . . . . . . 17 coeff coeff
3833, 37dgrlt 20137 . . . . . . . . . . . . . . . 16 Poly deg deg deg deg deg coeffdeg
3916, 30, 38syl2anc 643 . . . . . . . . . . . . . . 15 deg deg deg deg coeffdeg
4036, 39mpbid 202 . . . . . . . . . . . . . 14 deg deg coeffdeg
4140simpld 446 . . . . . . . . . . . . 13 deg deg
42 plydiveu.qd . . . . . . . . . . . . . . 15 deg deg
43 eqid 2404 . . . . . . . . . . . . . . . . 17 coeff coeff
4432, 43dgrlt 20137 . . . . . . . . . . . . . . . 16 Poly deg deg deg deg deg coeffdeg
4512, 30, 44syl2anc 643 . . . . . . . . . . . . . . 15 deg deg deg deg coeffdeg
4642, 45mpbid 202 . . . . . . . . . . . . . 14 deg deg coeffdeg
4746simpld 446 . . . . . . . . . . . . 13 deg deg
48 breq1 4175 . . . . . . . . . . . . . 14 deg deg deg deg deg deg deg deg deg deg deg deg
49 breq1 4175 . . . . . . . . . . . . . 14 deg deg deg deg deg deg deg deg deg deg deg deg
5048, 49ifboth 3730 . . . . . . . . . . . . 13 deg deg deg deg deg deg deg deg deg
5141, 47, 50syl2anc 643 . . . . . . . . . . . 12 deg deg deg deg deg
5220, 28, 31, 35, 51letrd 9183 . . . . . . . . . . 11 deg deg
5352adantr 452 . . . . . . . . . 10 deg deg
5413, 2, 3, 4, 6plysub 20091 . . . . . . . . . . . . . 14 Poly
55 dgrcl 20105 . . . . . . . . . . . . . 14 Poly deg
5654, 55syl 16 . . . . . . . . . . . . 13 deg
57 nn0addge1 10222 . . . . . . . . . . . . 13 deg deg deg deg deg
5831, 56, 57syl2anc 643 . . . . . . . . . . . 12 deg deg deg
5958adantr 452 . . . . . . . . . . 11 deg deg deg
60 plyf 20070 . . . . . . . . . . . . . . . . . . . 20 Poly
617, 60syl 16 . . . . . . . . . . . . . . . . . . 19
6261ffvelrnda 5829 . . . . . . . . . . . . . . . . . 18
638, 2, 3, 4plymul 20090 . . . . . . . . . . . . . . . . . . . 20 Poly
64 plyf 20070 . . . . . . . . . . . . . . . . . . . 20 Poly
6563, 64syl 16 . . . . . . . . . . . . . . . . . . 19
6665ffvelrnda 5829 . . . . . . . . . . . . . . . . . 18
678, 13, 3, 4plymul 20090 . . . . . . . . . . . . . . . . . . . 20 Poly
68 plyf 20070 . . . . . . . . . . . . . . . . . . . 20 Poly
6967, 68syl 16 . . . . . . . . . . . . . . . . . . 19
7069ffvelrnda 5829 . . . . . . . . . . . . . . . . . 18
7162, 66, 70nnncan1d 9401 . . . . . . . . . . . . . . . . 17
7271mpteq2dva 4255 . . . . . . . . . . . . . . . 16
73 cnex 9027 . . . . . . . . . . . . . . . . . 18
7473a1i 11 . . . . . . . . . . . . . . . . 17
7562, 66subcld 9367 . . . . . . . . . . . . . . . . 17
7662, 70subcld 9367 . . . . . . . . . . . . . . . . 17
7761feqmptd 5738 . . . . . . . . . . . . . . . . . . 19
7865feqmptd 5738 . . . . . . . . . . . . . . . . . . 19
7974, 62, 66, 77, 78offval2 6281 . . . . . . . . . . . . . . . . . 18
8010, 79syl5eq 2448 . . . . . . . . . . . . . . . . 17
8169feqmptd 5738 . . . . . . . . . . . . . . . . . . 19
8274, 62, 70, 77, 81offval2 6281 . . . . . . . . . . . . . . . . . 18
8314, 82syl5eq 2448 . . . . . . . . . . . . . . . . 17
8474, 75, 76, 80, 83offval2 6281 . . . . . . . . . . . . . . . 16
8574, 70, 66, 81, 78offval2 6281 . . . . . . . . . . . . . . . 16
8672, 84, 853eqtr4d 2446 . . . . . . . . . . . . . . 15
87 plyf 20070 . . . . . . . . . . . . . . . . 17 Poly
888, 87syl 16 . . . . . . . . . . . . . . . 16
89 plyf 20070 . . . . . . . . . . . . . . . . 17 Poly
9013, 89syl 16 . . . . . . . . . . . . . . . 16
91 plyf 20070 . . . . . . . . . . . . . . . . 17 Poly
922, 91syl 16 . . . . . . . . . . . . . . . 16
93 subdi 9423 . . . . . . . . . . . . . . . . 17
9493adantl 453 . . . . . . . . . . . . . . . 16
9574, 88, 90, 92, 94caofdi 6299 . . . . . . . . . . . . . . 15
9686, 95eqtr4d 2439 . . . . . . . . . . . . . 14
9796fveq2d 5691 . . . . . . . . . . . . 13 deg deg
9897adantr 452 . . . . . . . . . . . 12 deg deg
998adantr 452 . . . . . . . . . . . . 13 Poly
1009adantr 452 . . . . . . . . . . . . 13
10154adantr 452 . . . . . . . . . . . . 13 Poly
102 simpr 448 . . . . . . . . . . . . 13
103 eqid 2404 . . . . . . . . . . . . . 14 deg deg
104 eqid 2404 . . . . . . . . . . . . . 14 deg deg
105103, 104dgrmul 20141 . . . . . . . . . . . . 13 Poly Poly deg deg deg
10699, 100, 101, 102, 105syl22anc 1185 . . . . . . . . . . . 12 deg deg deg
10798, 106eqtrd 2436 . . . . . . . . . . 11 deg deg deg
10859, 107breqtrrd 4198 . . . . . . . . . 10 deg deg
10920, 31letri3d 9171 . . . . . . . . . . 11 deg deg deg deg deg deg
110109adantr 452 . . . . . . . . . 10 deg deg deg deg deg deg
11153, 108, 110mpbir2and 889 . . . . . . . . 9 deg deg
112111fveq2d 5691 . . . . . . . 8 coeff deg coeff deg
11343, 37coesub 20128 . . . . . . . . . . . . 13 Poly Poly coeff coeff coeff
11412, 16, 113syl2anc 643 . . . . . . . . . . . 12 coeff coeff coeff
115114fveq1d 5689 . . . . . . . . . . 11 coeff deg coeff coeffdeg
11643coef3 20104 . . . . . . . . . . . . . 14 Poly coeff
117 ffn 5550 . . . . . . . . . . . . . 14 coeff coeff
11812, 116, 1173syl 19 . . . . . . . . . . . . 13 coeff
11937coef3 20104 . . . . . . . . . . . . . 14 Poly coeff
120 ffn 5550 . . . . . . . . . . . . . 14 coeff coeff
12116, 119, 1203syl 19 . . . . . . . . . . . . 13 coeff
122 nn0ex 10183 . . . . . . . . . . . . . 14
123122a1i 11 . . . . . . . . . . . . 13
124 inidm 3510 . . . . . . . . . . . . 13
12546simprd 450 . . . . . . . . . . . . . 14 coeffdeg
126125adantr 452 . . . . . . . . . . . . 13 deg coeffdeg
12740simprd 450 . . . . . . . . . . . . . 14 coeffdeg
128127adantr 452 . . . . . . . . . . . . 13 deg coeffdeg
129118, 121, 123, 123, 124, 126, 128ofval 6273 . . . . . . . . . . . 12 deg coeff coeffdeg
13030, 129mpdan 650 . . . . . . . . . . 11 coeff coeffdeg
131115, 130eqtrd 2436 . . . . . . . . . 10 coeff deg
132 0cn 9040 . . . . . . . . . . 11
133132subidi 9327 . . . . . . . . . 10
134131, 133syl6eq 2452 . . . . . . . . 9 coeff deg
135134adantr 452 . . . . . . . 8 coeff deg
136112, 135eqtrd 2436 . . . . . . 7 coeff deg
137 eqid 2404 . . . . . . . . . 10 deg deg
138 eqid 2404 . . . . . . . . . 10 coeff coeff
139137, 138dgreq0 20136 . . . . . . . . 9 Poly coeff deg
14017, 139syl 16 . . . . . . . 8 coeff deg
141140biimpar 472 . . . . . . 7 coeff deg
142136, 141syldan 457 . . . . . 6
143142ex 424 . . . . 5
144 plymul0or 20151 . . . . . . 7 Poly Poly
1458, 54, 144syl2anc 643 . . . . . 6
14696eqeq1d 2412 . . . . . 6
1479neneqd 2583 . . . . . . 7
148 biorf 395 . . . . . . 7
149147, 148syl 16 . . . . . 6
150145, 146, 1493bitr4d 277 . . . . 5
151143, 150sylibd 206 . . . 4
1521, 151pm2.61dne 2644 . . 3
153 df-0p 19515 . . 3
154152, 153syl6eq 2452 . 2
155 ofsubeq0 9953 . . 3
15674, 90, 92, 155syl3anc 1184 . 2
157154, 156mpbid 202 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wo 358   wa 359   w3a 936   wceq 1649   wcel 1721   wne 2567  cvv 2916  cif 3699  csn 3774   class class class wbr 4172   cmpt 4226   cxp 4835   wfn 5408  wf 5409  cfv 5413  (class class class)co 6040   cof 6262  cc 8944  cr 8945  cc0 8946  c1 8947   caddc 8949   cmul 8951   clt 9076   cle 9077   cmin 9247  cneg 9248   cdiv 9633  cn0 10177  c0p 19514  Polycply 20056  coeffccoe 20058  degcdgr 20059 This theorem is referenced by:  plydivalg  20169 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 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025 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 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-oi 7435  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-rp 10569  df-fz 11000  df-fzo 11091  df-fl 11157  df-seq 11279  df-exp 11338  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-clim 12237  df-rlim 12238  df-sum 12435  df-0p 19515  df-ply 20060  df-coe 20062  df-dgr 20063
 Copyright terms: Public domain W3C validator