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

Theorem plydivlem4 23236
 Description: Lemma for plydivex 23237. Induction step. (Contributed by Mario Carneiro, 26-Jul-2014.)
Hypotheses
Ref Expression
plydiv.pl
plydiv.tm
plydiv.rc
plydiv.m1
plydiv.f Poly
plydiv.g Poly
plydiv.z
plydiv.r
plydiv.d
plydiv.e
plydiv.fz
plydiv.u
plydiv.h
plydiv.al Poly deg Poly deg
plydiv.a coeff
plydiv.b coeff
plydiv.m deg
plydiv.n deg
Assertion
Ref Expression
plydivlem4 Poly deg
Distinct variable groups:   ,,,   ,,,,,,   ,,,,,,   ,,,   ,,,   ,,   ,,,   ,,,,,,   ,,,,,,   ,,,,   ,,,,,,   ,
Allowed substitution hints:   (,)   (,,)   (,,)   (,,,)   (,)   (,,,,,)   (,,)

Proof of Theorem plydivlem4
StepHypRef Expression
1 plydiv.f . . . . . . . 8 Poly
2 plybss 23135 . . . . . . . 8 Poly
31, 2syl 17 . . . . . . 7
4 plydiv.pl . . . . . . . . . . . . 13
5 plydiv.tm . . . . . . . . . . . . 13
6 plydiv.rc . . . . . . . . . . . . 13
7 plydiv.m1 . . . . . . . . . . . . 13
84, 5, 6, 7plydivlem1 23233 . . . . . . . . . . . 12
9 plydiv.a . . . . . . . . . . . . 13 coeff
109coef2 23172 . . . . . . . . . . . 12 Poly
111, 8, 10syl2anc 665 . . . . . . . . . . 11
12 plydiv.m . . . . . . . . . . . 12 deg
13 dgrcl 23174 . . . . . . . . . . . . 13 Poly deg
141, 13syl 17 . . . . . . . . . . . 12 deg
1512, 14syl5eqel 2514 . . . . . . . . . . 11
1611, 15ffvelrnd 6035 . . . . . . . . . 10
173, 16sseldd 3465 . . . . . . . . 9
18 plydiv.g . . . . . . . . . . . 12 Poly
19 plydiv.b . . . . . . . . . . . . 13 coeff
2019coef2 23172 . . . . . . . . . . . 12 Poly
2118, 8, 20syl2anc 665 . . . . . . . . . . 11
22 plydiv.n . . . . . . . . . . . 12 deg
23 dgrcl 23174 . . . . . . . . . . . . 13 Poly deg
2418, 23syl 17 . . . . . . . . . . . 12 deg
2522, 24syl5eqel 2514 . . . . . . . . . . 11
2621, 25ffvelrnd 6035 . . . . . . . . . 10
273, 26sseldd 3465 . . . . . . . . 9
28 plydiv.z . . . . . . . . . 10
2922, 19dgreq0 23206 . . . . . . . . . . . 12 Poly
3018, 29syl 17 . . . . . . . . . . 11
3130necon3bid 2682 . . . . . . . . . 10
3228, 31mpbid 213 . . . . . . . . 9
3317, 27, 32divrecd 10387 . . . . . . . 8
34 fvex 5888 . . . . . . . . . . . 12
35 eleq1 2494 . . . . . . . . . . . . . . 15
36 neeq1 2705 . . . . . . . . . . . . . . 15
3735, 36anbi12d 715 . . . . . . . . . . . . . 14
3837anbi2d 708 . . . . . . . . . . . . 13
39 oveq2 6310 . . . . . . . . . . . . . 14
4039eleq1d 2491 . . . . . . . . . . . . 13
4138, 40imbi12d 321 . . . . . . . . . . . 12
4234, 41, 6vtocl 3133 . . . . . . . . . . 11
4342ex 435 . . . . . . . . . 10
4426, 32, 43mp2and 683 . . . . . . . . 9
455, 16, 44caovcld 6473 . . . . . . . 8
4633, 45eqeltrd 2510 . . . . . . 7
47 plydiv.d . . . . . . 7
48 plydiv.h . . . . . . . 8
4948ply1term 23145 . . . . . . 7 Poly
503, 46, 47, 49syl3anc 1264 . . . . . 6 Poly
5150adantr 466 . . . . 5 Poly Poly
52 simpr 462 . . . . 5 Poly Poly
534adantlr 719 . . . . 5 Poly
5451, 52, 53plyadd 23158 . . . 4 Poly Poly
5554adantr 466 . . 3 Poly deg Poly
56 cnex 9621 . . . . . . . . 9
5756a1i 11 . . . . . . . 8 Poly
581adantr 466 . . . . . . . . 9 Poly Poly
59 plyf 23139 . . . . . . . . 9 Poly
6058, 59syl 17 . . . . . . . 8 Poly
61 mulcl 9624 . . . . . . . . . 10
6261adantl 467 . . . . . . . . 9 Poly
63 plyf 23139 . . . . . . . . . 10 Poly
6451, 63syl 17 . . . . . . . . 9 Poly
6518adantr 466 . . . . . . . . . 10 Poly Poly
66 plyf 23139 . . . . . . . . . 10 Poly
6765, 66syl 17 . . . . . . . . 9 Poly
68 inidm 3671 . . . . . . . . 9
6962, 64, 67, 57, 57, 68off 6557 . . . . . . . 8 Poly
70 plyf 23139 . . . . . . . . . 10 Poly
7170adantl 467 . . . . . . . . 9 Poly
7262, 67, 71, 57, 57, 68off 6557 . . . . . . . 8 Poly
73 subsub4 9908 . . . . . . . . 9
7473adantl 467 . . . . . . . 8 Poly
7557, 60, 69, 72, 74caofass 6576 . . . . . . 7 Poly
76 mulcom 9626 . . . . . . . . . . . 12
7776adantl 467 . . . . . . . . . . 11 Poly
7857, 64, 67, 77caofcom 6574 . . . . . . . . . 10 Poly
7978oveq1d 6317 . . . . . . . . 9 Poly
80 adddi 9629 . . . . . . . . . . 11
8180adantl 467 . . . . . . . . . 10 Poly
8257, 67, 64, 71, 81caofdi 6578 . . . . . . . . 9 Poly
8379, 82eqtr4d 2466 . . . . . . . 8 Poly
8483oveq2d 6318 . . . . . . 7 Poly
8575, 84eqtrd 2463 . . . . . 6 Poly
8685eqeq1d 2424 . . . . 5 Poly
8785fveq2d 5882 . . . . . 6 Poly deg deg
8887breq1d 4430 . . . . 5 Poly deg deg
8986, 88orbi12d 714 . . . 4 Poly deg deg
9089biimpa 486 . . 3 Poly deg deg
91 plydiv.r . . . . . . 7
92 oveq2 6310 . . . . . . . 8
9392oveq2d 6318 . . . . . . 7
9491, 93syl5eq 2475 . . . . . 6
9594eqeq1d 2424 . . . . 5
9694fveq2d 5882 . . . . . 6 deg deg
9796breq1d 4430 . . . . 5 deg deg
9895, 97orbi12d 714 . . . 4 deg deg
9998rspcev 3182 . . 3 Poly deg Poly deg
10055, 90, 99syl2anc 665 . 2 Poly deg Poly deg
10150, 18, 4, 5plymul 23159 . . . 4 Poly
1021, 101, 4, 5, 7plysub 23160 . . 3 Poly
103 plydiv.al . . 3 Poly deg Poly deg
104 eqid 2422 . . . . . . 7 deg deg
10512, 104dgrsub 23213 . . . . . 6 Poly Poly deg deg deg
1061, 101, 105syl2anc 665 . . . . 5 deg deg deg
107 plydiv.fz . . . . . . . . . . . . 13
10812, 9dgreq0 23206 . . . . . . . . . . . . . . 15 Poly
1091, 108syl 17 . . . . . . . . . . . . . 14
110109necon3bid 2682 . . . . . . . . . . . . 13
111107, 110mpbid 213 . . . . . . . . . . . 12
11217, 27, 111, 32divne0d 10400 . . . . . . . . . . 11
1133, 46sseldd 3465 . . . . . . . . . . . . 13
11448coe1term 23200 . . . . . . . . . . . . 13 coeff
115113, 47, 47, 114syl3anc 1264 . . . . . . . . . . . 12 coeff
116 eqid 2422 . . . . . . . . . . . . 13
117116iftruei 3916 . . . . . . . . . . . 12
118115, 117syl6eq 2479 . . . . . . . . . . 11 coeff
119 c0ex 9638 . . . . . . . . . . . . 13
120119fvconst2 6132 . . . . . . . . . . . 12
12147, 120syl 17 . . . . . . . . . . 11
122112, 118, 1213netr4d 2729 . . . . . . . . . 10 coeff
123 fveq2 5878 . . . . . . . . . . . . 13 coeff coeff
124 coe0 23197 . . . . . . . . . . . . 13 coeff
125123, 124syl6eq 2479 . . . . . . . . . . . 12 coeff
126125fveq1d 5880 . . . . . . . . . . 11 coeff
127126necon3i 2664 . . . . . . . . . 10 coeff
128122, 127syl 17 . . . . . . . . 9
129 eqid 2422 . . . . . . . . . 10 deg deg
130129, 22dgrmul 23211 . . . . . . . . 9 Poly Poly deg deg
13150, 128, 18, 28, 130syl22anc 1265 . . . . . . . 8 deg deg
13248dgr1term 23201 . . . . . . . . . . . 12 deg
133113, 112, 47, 132syl3anc 1264 . . . . . . . . . . 11 deg
134 plydiv.e . . . . . . . . . . 11
135133, 134eqtr4d 2466 . . . . . . . . . 10 deg
136135oveq1d 6317 . . . . . . . . 9 deg
13715nn0cnd 10928 . . . . . . . . . 10
13825nn0cnd 10928 . . . . . . . . . 10
139137, 138npcand 9991 . . . . . . . . 9
140136, 139eqtrd 2463 . . . . . . . 8 deg
141131, 140eqtrd 2463 . . . . . . 7 deg
142141ifeq1d 3927 . . . . . 6 deg deg deg
143 ifid 3946 . . . . . 6 deg
144142, 143syl6eq 2479 . . . . 5 deg deg
145106, 144breqtrd 4445 . . . 4 deg
146 eqid 2422 . . . . . . . 8 coeff coeff
1479, 146coesub 23198 . . . . . . 7 Poly Poly coeff coeff
1481, 101, 147syl2anc 665 . . . . . 6 coeff coeff
149148fveq1d 5880 . . . . 5 coeff coeff
1509coef3 23173 . . . . . . . 8 Poly
151 ffn 5743 . . . . . . . 8
1521, 150, 1513syl 18 . . . . . . 7
153146coef3 23173 . . . . . . . 8 Poly coeff
154 ffn 5743 . . . . . . . 8 coeff coeff
155101, 153, 1543syl 18 . . . . . . 7 coeff
156 nn0ex 10876 . . . . . . . 8
157156a1i 11 . . . . . . 7
158 inidm 3671 . . . . . . 7
159 eqidd 2423 . . . . . . 7
160 eqid 2422 . . . . . . . . . . 11 coeff coeff
161160, 19, 129, 22coemulhi 23195 . . . . . . . . . 10 Poly Poly coeff deg coeffdeg
16250, 18, 161syl2anc 665 . . . . . . . . 9 coeff deg coeffdeg
163140fveq2d 5882 . . . . . . . . 9 coeff deg coeff
164133fveq2d 5882 . . . . . . . . . . . 12 coeffdeg coeff
165164, 118eqtrd 2463 . . . . . . . . . . 11 coeffdeg
166165oveq1d 6317 . . . . . . . . . 10 coeffdeg
16717, 27, 32divcan1d 10385 . . . . . . . . . 10
168166, 167eqtrd 2463 . . . . . . . . 9 coeffdeg
169162, 163, 1683eqtr3d 2471 . . . . . . . 8 coeff
170169adantr 466 . . . . . . 7 coeff
171152, 155, 157, 157, 158, 159, 170ofval 6551 . . . . . 6 coeff
17215, 171mpdan 672 . . . . 5 coeff
17317subidd 9975 . . . . 5
174149, 172, 1733eqtrd 2467 . . . 4 coeff
175 dgrcl 23174 . . . . . . . . . 10 Poly deg
176102, 175syl 17 . . . . . . . . 9 deg
177176nn0red 10927 . . . . . . . 8 deg
17815nn0red 10927 . . . . . . . 8
17925nn0red 10927 . . . . . . . 8
180177, 178, 179ltsub1d 10223 . . . . . . 7 deg deg
181134breq2d 4432 . . . . . . 7 deg deg
182180, 181bitrd 256 . . . . . 6 deg deg
183182orbi2d 706 . . . . 5 deg deg
184 eqid 2422 . . . . . . 7 deg deg
185 eqid 2422 . . . . . . 7 coeff coeff
186184, 185dgrlt 23207 . . . . . 6 Poly deg deg coeff
187102, 15, 186syl2anc 665 . . . . 5 deg deg coeff
188183, 187bitr3d 258 . . . 4 deg deg coeff
189145, 174, 188mpbir2and 930 . . 3 deg
190 eqeq1 2426 . . . . . 6
191 fveq2 5878 . . . . . . . 8 deg deg
192191oveq1d 6317 . . . . . . 7 deg deg
193192breq1d 4430 . . . . . 6 deg deg
194190, 193orbi12d 714 . . . . 5 deg deg
195 plydiv.u . . . . . . . . 9
196 oveq1 6309 . . . . . . . . 9
197195, 196syl5eq 2475 . . . . . . . 8
198197eqeq1d 2424 . . . . . . 7
199197fveq2d 5882 . . . . . . . 8 deg deg
200199breq1d 4430 . . . . . . 7 deg deg
201198, 200orbi12d 714 . . . . . 6 deg deg
202201rexbidv 2939 . . . . 5 Poly deg Poly deg
203194, 202imbi12d 321 . . . 4 deg Poly deg deg Poly deg
204203rspcv 3178 . . 3 Poly Poly deg Poly deg deg Poly deg
205102, 103, 189, 204syl3c 63 . 2 Poly deg
206100, 205r19.29a 2970 1 Poly deg
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wo 369   wa 370   w3a 982   wceq 1437   wcel 1868   wne 2618  wral 2775  wrex 2776  cvv 3081   wss 3436  cif 3909  csn 3996   class class class wbr 4420   cmpt 4479   cxp 4848   wfn 5593  wf 5594  cfv 5598  (class class class)co 6302   cof 6540  cc 9538  cc0 9540  c1 9541   caddc 9543   cmul 9545   clt 9676   cle 9677   cmin 9861  cneg 9862   cdiv 10270  cn0 10870  cexp 12272  c0p 22614  Polycply 23125  coeffccoe 23127  degcdgr 23128 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594  ax-inf2 8149  ax-cnex 9596  ax-resscn 9597  ax-1cn 9598  ax-icn 9599  ax-addcl 9600  ax-addrcl 9601  ax-mulcl 9602  ax-mulrcl 9603  ax-mulcom 9604  ax-addass 9605  ax-mulass 9606  ax-distr 9607  ax-i2m1 9608  ax-1ne0 9609  ax-1rid 9610  ax-rnegex 9611  ax-rrecex 9612  ax-cnre 9613  ax-pre-lttri 9614  ax-pre-lttrn 9615  ax-pre-ltadd 9616  ax-pre-mulgt0 9617  ax-pre-sup 9618  ax-addf 9619 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4761  df-id 4765  df-po 4771  df-so 4772  df-fr 4809  df-se 4810  df-we 4811  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-pred 5396  df-ord 5442  df-on 5443  df-lim 5444  df-suc 5445  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-isom 5607  df-riota 6264  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-of 6542  df-om 6704  df-1st 6804  df-2nd 6805  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-oadd 7191  df-er 7368  df-map 7479  df-pm 7480  df-en 7575  df-dom 7576  df-sdom 7577  df-fin 7578  df-sup 7959  df-inf 7960  df-oi 8028  df-card 8375  df-pnf 9678  df-mnf 9679  df-xr 9680  df-ltxr 9681  df-le 9682  df-sub 9863  df-neg 9864  df-div 10271  df-nn 10611  df-2 10669  df-3 10670  df-n0 10871  df-z 10939  df-uz 11161  df-rp 11304  df-fz 11786  df-fzo 11917  df-fl 12028  df-seq 12214  df-exp 12273  df-hash 12516  df-cj 13151  df-re 13152  df-im 13153  df-sqrt 13287  df-abs 13288  df-clim 13540  df-rlim 13541  df-sum 13741  df-0p 22615  df-ply 23129  df-coe 23131  df-dgr 23132 This theorem is referenced by:  plydivex  23237
 Copyright terms: Public domain W3C validator