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

 Description: Lemma for coeadd 23142 and dgradd 23158. (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 23111 . . 3 Poly Poly Poly
2 coeadd.4 . . . . . 6 deg
3 dgrcl 23124 . . . . . 6 Poly deg
42, 3syl5eqel 2505 . . . . 5 Poly
54adantl 467 . . . 4 Poly Poly
6 coeadd.3 . . . . . 6 deg
7 dgrcl 23124 . . . . . 6 Poly deg
86, 7syl5eqel 2505 . . . . 5 Poly
98adantr 466 . . . 4 Poly Poly
105, 9ifcld 3892 . . 3 Poly Poly
11 addcl 9567 . . . . 5
1211adantl 467 . . . 4 Poly Poly
13 coefv0.1 . . . . . 6 coeff
1413coef3 23123 . . . . 5 Poly
1514adantr 466 . . . 4 Poly Poly
16 coeadd.2 . . . . . 6 coeff
1716coef3 23123 . . . . 5 Poly
1817adantl 467 . . . 4 Poly Poly
19 nn0ex 10821 . . . . 5
2019a1i 11 . . . 4 Poly Poly
21 inidm 3609 . . . 4
2212, 15, 18, 20, 20, 21off 6499 . . 3 Poly Poly
23 oveq12 6253 . . . . . . . . . 10
24 00id 9754 . . . . . . . . . 10
2523, 24syl6eq 2473 . . . . . . . . 9
26 ffn 5684 . . . . . . . . . . . 12
2715, 26syl 17 . . . . . . . . . . 11 Poly Poly
28 ffn 5684 . . . . . . . . . . . 12
2918, 28syl 17 . . . . . . . . . . 11 Poly Poly
30 eqidd 2424 . . . . . . . . . . 11 Poly Poly
31 eqidd 2424 . . . . . . . . . . 11 Poly Poly
3227, 29, 20, 20, 21, 30, 31ofval 6493 . . . . . . . . . 10 Poly Poly
3332eqeq1d 2425 . . . . . . . . 9 Poly Poly
3425, 33syl5ibr 224 . . . . . . . 8 Poly Poly
3534necon3ad 2609 . . . . . . 7 Poly Poly
36 neorian 2690 . . . . . . 7
3735, 36syl6ibr 230 . . . . . 6 Poly Poly
3813, 6dgrub2 23126 . . . . . . . . . . 11 Poly
3938adantr 466 . . . . . . . . . 10 Poly Poly
40 plyco0 23083 . . . . . . . . . . 11
419, 15, 40syl2anc 665 . . . . . . . . . 10 Poly Poly
4239, 41mpbid 213 . . . . . . . . 9 Poly Poly
4342r19.21bi 2729 . . . . . . . 8 Poly Poly
449adantr 466 . . . . . . . . . . 11 Poly Poly
4544nn0red 10872 . . . . . . . . . 10 Poly Poly
465adantr 466 . . . . . . . . . . 11 Poly Poly
4746nn0red 10872 . . . . . . . . . 10 Poly Poly
48 max1 11426 . . . . . . . . . 10
4945, 47, 48syl2anc 665 . . . . . . . . 9 Poly Poly
50 nn0re 10824 . . . . . . . . . . 11
5150adantl 467 . . . . . . . . . 10 Poly Poly
5210adantr 466 . . . . . . . . . . 11 Poly Poly
5352nn0red 10872 . . . . . . . . . 10 Poly Poly
54 letr 9673 . . . . . . . . . 10
5551, 45, 53, 54syl3anc 1264 . . . . . . . . 9 Poly Poly
5649, 55mpan2d 678 . . . . . . . 8 Poly Poly
5743, 56syld 45 . . . . . . 7 Poly Poly
5816, 2dgrub2 23126 . . . . . . . . . . 11 Poly
5958adantl 467 . . . . . . . . . 10 Poly Poly
60 plyco0 23083 . . . . . . . . . . 11
615, 18, 60syl2anc 665 . . . . . . . . . 10 Poly Poly
6259, 61mpbid 213 . . . . . . . . 9 Poly Poly
6362r19.21bi 2729 . . . . . . . 8 Poly Poly
64 max2 11428 . . . . . . . . . 10
6545, 47, 64syl2anc 665 . . . . . . . . 9 Poly Poly
66 letr 9673 . . . . . . . . . 10
6751, 47, 53, 66syl3anc 1264 . . . . . . . . 9 Poly Poly
6865, 67mpan2d 678 . . . . . . . 8 Poly Poly
6963, 68syld 45 . . . . . . 7 Poly Poly
7057, 69jaod 381 . . . . . 6 Poly Poly
7137, 70syld 45 . . . . 5 Poly Poly
7271ralrimiva 2774 . . . 4 Poly Poly
73 plyco0 23083 . . . . 5
7410, 22, 73syl2anc 665 . . . 4 Poly Poly
7572, 74mpbird 235 . . 3 Poly Poly
76 simpl 458 . . . 4 Poly Poly Poly
77 simpr 462 . . . 4 Poly Poly Poly
7813, 6coeid 23129 . . . . 5 Poly
7978adantr 466 . . . 4 Poly Poly
8016, 2coeid 23129 . . . . 5 Poly
8180adantl 467 . . . 4 Poly Poly
8276, 77, 9, 5, 15, 18, 39, 59, 79, 81plyaddlem1 23104 . . 3 Poly Poly
831, 10, 22, 75, 82coeeq 23118 . 2 Poly Poly coeff
84 elfznn0 11833 . . . 4
85 ffvelrn 5974 . . . 4
8622, 84, 85syl2an 479 . . 3 Poly Poly
871, 10, 86, 82dgrle 23134 . 2 Poly Poly deg
8883, 87jca 534 1 Poly Poly coeff deg
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wo 369   wa 370   wceq 1437   wcel 1872   wne 2594  wral 2709  cvv 3017  cif 3849  csn 3936   class class class wbr 4361   cmpt 4420  cima 4794   wfn 5534  wf 5535  cfv 5539  (class class class)co 6244   cof 6482  cc 9483  cr 9484  cc0 9485  c1 9486   caddc 9488   cmul 9490   cle 9622  cn0 10815  cuz 11105  cfz 11730  cexp 12217  csu 13690  Polycply 23075  coeffccoe 23077  degcdgr 23078 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-inf2 8094  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562  ax-pre-sup 9563  ax-addf 9564 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 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-int 4194  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-se 4751  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-isom 5548  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-of 6484  df-om 6646  df-1st 6746  df-2nd 6747  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-1o 7132  df-oadd 7136  df-er 7313  df-map 7424  df-pm 7425  df-en 7520  df-dom 7521  df-sdom 7522  df-fin 7523  df-sup 7904  df-inf 7905  df-oi 7973  df-card 8320  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-div 10216  df-nn 10556  df-2 10614  df-3 10615  df-n0 10816  df-z 10884  df-uz 11106  df-rp 11249  df-fz 11731  df-fzo 11862  df-fl 11973  df-seq 12159  df-exp 12218  df-hash 12461  df-cj 13101  df-re 13102  df-im 13103  df-sqrt 13237  df-abs 13238  df-clim 13490  df-rlim 13491  df-sum 13691  df-0p 22565  df-ply 23079  df-coe 23081  df-dgr 23082 This theorem is referenced by:  coeadd  23142  dgradd  23158
 Copyright terms: Public domain W3C validator