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

 Description: Lemma for coeadd 20108 and dgradd 20124. (Contributed by Mario Carneiro, 24-Jul-2014.)
Hypotheses
Ref Expression
coefv0.1 coeff
Assertion
Ref Expression

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 plyaddcl 20078 . . 3 Poly Poly Poly
2 coeadd.4 . . . . . 6 deg
3 dgrcl 20091 . . . . . 6 Poly deg
42, 3syl5eqel 2485 . . . . 5 Poly
54adantl 453 . . . 4 Poly Poly
6 coeadd.3 . . . . . 6 deg
7 dgrcl 20091 . . . . . 6 Poly deg
86, 7syl5eqel 2485 . . . . 5 Poly
98adantr 452 . . . 4 Poly Poly
10 ifcl 3732 . . . 4
115, 9, 10syl2anc 643 . . 3 Poly Poly
12 addcl 9019 . . . . 5
1312adantl 453 . . . 4 Poly Poly
14 coefv0.1 . . . . . 6 coeff
1514coef3 20090 . . . . 5 Poly
1615adantr 452 . . . 4 Poly Poly
17 coeadd.2 . . . . . 6 coeff
1817coef3 20090 . . . . 5 Poly
1918adantl 453 . . . 4 Poly Poly
20 nn0ex 10173 . . . . 5
2120a1i 11 . . . 4 Poly Poly
22 inidm 3507 . . . 4
2313, 16, 19, 21, 21, 22off 6273 . . 3 Poly Poly
24 oveq12 6043 . . . . . . . . . 10
25 00id 9187 . . . . . . . . . 10
2624, 25syl6eq 2449 . . . . . . . . 9
27 ffn 5545 . . . . . . . . . . . 12
2816, 27syl 16 . . . . . . . . . . 11 Poly Poly
29 ffn 5545 . . . . . . . . . . . 12
3019, 29syl 16 . . . . . . . . . . 11 Poly Poly
31 eqidd 2402 . . . . . . . . . . 11 Poly Poly
32 eqidd 2402 . . . . . . . . . . 11 Poly Poly
3328, 30, 21, 21, 22, 31, 32ofval 6267 . . . . . . . . . 10 Poly Poly
3433eqeq1d 2409 . . . . . . . . 9 Poly Poly
3526, 34syl5ibr 213 . . . . . . . 8 Poly Poly
3635necon3ad 2600 . . . . . . 7 Poly Poly
37 neorian 2651 . . . . . . 7
3836, 37syl6ibr 219 . . . . . 6 Poly Poly
3914, 6dgrub2 20093 . . . . . . . . . . 11 Poly
4039adantr 452 . . . . . . . . . 10 Poly Poly
41 plyco0 20050 . . . . . . . . . . 11
429, 16, 41syl2anc 643 . . . . . . . . . 10 Poly Poly
4340, 42mpbid 202 . . . . . . . . 9 Poly Poly
4443r19.21bi 2761 . . . . . . . 8 Poly Poly
459adantr 452 . . . . . . . . . . 11 Poly Poly
4645nn0red 10221 . . . . . . . . . 10 Poly Poly
475adantr 452 . . . . . . . . . . 11 Poly Poly
4847nn0red 10221 . . . . . . . . . 10 Poly Poly
49 max1 10719 . . . . . . . . . 10
5046, 48, 49syl2anc 643 . . . . . . . . 9 Poly Poly
51 nn0re 10176 . . . . . . . . . . 11
5251adantl 453 . . . . . . . . . 10 Poly Poly
5311adantr 452 . . . . . . . . . . 11 Poly Poly
5453nn0red 10221 . . . . . . . . . 10 Poly Poly
55 letr 9114 . . . . . . . . . 10
5652, 46, 54, 55syl3anc 1184 . . . . . . . . 9 Poly Poly
5750, 56mpan2d 656 . . . . . . . 8 Poly Poly
5844, 57syld 42 . . . . . . 7 Poly Poly
5917, 2dgrub2 20093 . . . . . . . . . . 11 Poly
6059adantl 453 . . . . . . . . . 10 Poly Poly
61 plyco0 20050 . . . . . . . . . . 11
625, 19, 61syl2anc 643 . . . . . . . . . 10 Poly Poly
6360, 62mpbid 202 . . . . . . . . 9 Poly Poly
6463r19.21bi 2761 . . . . . . . 8 Poly Poly
65 max2 10721 . . . . . . . . . 10
6646, 48, 65syl2anc 643 . . . . . . . . 9 Poly Poly
67 letr 9114 . . . . . . . . . 10
6852, 48, 54, 67syl3anc 1184 . . . . . . . . 9 Poly Poly
6966, 68mpan2d 656 . . . . . . . 8 Poly Poly
7064, 69syld 42 . . . . . . 7 Poly Poly
7158, 70jaod 370 . . . . . 6 Poly Poly
7238, 71syld 42 . . . . 5 Poly Poly
7372ralrimiva 2746 . . . 4 Poly Poly
74 plyco0 20050 . . . . 5
7511, 23, 74syl2anc 643 . . . 4 Poly Poly
7673, 75mpbird 224 . . 3 Poly Poly
77 simpl 444 . . . 4 Poly Poly Poly
78 simpr 448 . . . 4 Poly Poly Poly
7914, 6coeid 20096 . . . . 5 Poly
8079adantr 452 . . . 4 Poly Poly
8117, 2coeid 20096 . . . . 5 Poly
8281adantl 453 . . . 4 Poly Poly
8377, 78, 9, 5, 16, 19, 40, 60, 80, 82plyaddlem1 20071 . . 3 Poly Poly
841, 11, 23, 76, 83coeeq 20085 . 2 Poly Poly coeff
85 elfznn0 11029 . . . 4
86 ffvelrn 5821 . . . 4
8723, 85, 86syl2an 464 . . 3 Poly Poly
881, 11, 87, 83dgrle 20101 . 2 Poly Poly deg
8984, 88jca 519 1 Poly Poly coeff deg
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wo 358   wa 359   wceq 1649   wcel 1721   wne 2564  wral 2663  cvv 2913  cif 3696  csn 3771   class class class wbr 4167   cmpt 4221  cima 4835   wfn 5403  wf 5404  cfv 5408  (class class class)co 6034   cof 6256  cc 8935  cr 8936  cc0 8937  c1 8938   caddc 8940   cmul 8942   cle 9068  cn0 10167  cuz 10434  cfz 10989  cexp 11323  csu 12420  Polycply 20042  coeffccoe 20044  degcdgr 20045 This theorem is referenced by:  coeadd  20108  dgradd  20124 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 2382  ax-rep 4275  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655  ax-inf2 7543  ax-cnex 8993  ax-resscn 8994  ax-1cn 8995  ax-icn 8996  ax-addcl 8997  ax-addrcl 8998  ax-mulcl 8999  ax-mulrcl 9000  ax-mulcom 9001  ax-addass 9002  ax-mulass 9003  ax-distr 9004  ax-i2m1 9005  ax-1ne0 9006  ax-1rid 9007  ax-rnegex 9008  ax-rrecex 9009  ax-cnre 9010  ax-pre-lttri 9011  ax-pre-lttrn 9012  ax-pre-ltadd 9013  ax-pre-mulgt0 9014  ax-pre-sup 9015  ax-addf 9016 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 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-nel 2567  df-ral 2668  df-rex 2669  df-reu 2670  df-rmo 2671  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-uni 3972  df-int 4007  df-iun 4051  df-br 4168  df-opab 4222  df-mpt 4223  df-tr 4258  df-eprel 4449  df-id 4453  df-po 4458  df-so 4459  df-fr 4496  df-se 4497  df-we 4498  df-ord 4539  df-on 4540  df-lim 4541  df-suc 4542  df-om 4800  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-isom 5417  df-ov 6037  df-oprab 6038  df-mpt2 6039  df-of 6258  df-1st 6302  df-2nd 6303  df-riota 6499  df-recs 6583  df-rdg 6618  df-1o 6674  df-oadd 6678  df-er 6855  df-map 6970  df-pm 6971  df-en 7060  df-dom 7061  df-sdom 7062  df-fin 7063  df-sup 7395  df-oi 7426  df-card 7773  df-pnf 9069  df-mnf 9070  df-xr 9071  df-ltxr 9072  df-le 9073  df-sub 9239  df-neg 9240  df-div 9624  df-nn 9947  df-2 10004  df-3 10005  df-n0 10168  df-z 10229  df-uz 10435  df-rp 10559  df-fz 10990  df-fzo 11080  df-fl 11143  df-seq 11265  df-exp 11324  df-hash 11560  df-cj 11845  df-re 11846  df-im 11847  df-sqr 11981  df-abs 11982  df-clim 12223  df-rlim 12224  df-sum 12421  df-0p 19501  df-ply 20046  df-coe 20048  df-dgr 20049
 Copyright terms: Public domain W3C validator