MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mdegleb Structured version   Visualization version   GIF version
Theorem mdegleb 25817
Description: Property of being of limited degree. (Contributed by Stefan O'Rear, 19-Mar-2015.)
Hypotheses
Ref Expression
mdegval.d 𝐷 = (𝐼 mDeg 𝑅)
mdegval.p 𝑃 = (𝐼 mPoly 𝑅)
mdegval.b 𝐡 = (Baseβ€˜π‘ƒ)
mdegval.z 0 = (0gβ€˜π‘…)
mdegval.a 𝐴 = {π‘š ∈ (β„•0 ↑m 𝐼) ∣ (β—‘π‘š β€œ β„•) ∈ Fin}
mdegval.h 𝐻 = (β„Ž ∈ 𝐴 ↦ (β„‚fld Ξ£g β„Ž))
Assertion
Ref Expression
mdegleb ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ ((π·β€˜πΉ) ≀ 𝐺 ↔ βˆ€π‘₯ ∈ 𝐴 (𝐺 < (π»β€˜π‘₯) β†’ (πΉβ€˜π‘₯) = 0 )))
Distinct variable groups:   𝐴,β„Ž   π‘š,𝐼   0 ,β„Ž   π‘₯,𝐴   π‘₯,𝐡   π‘₯,𝐹   π‘₯,𝐺   π‘₯,𝐻   β„Ž,𝐼   π‘₯,𝑅   π‘₯, 0   β„Ž,π‘š
Allowed substitution hints:   𝐴(π‘š)   𝐡(β„Ž,π‘š)   𝐷(π‘₯,β„Ž,π‘š)   𝑃(π‘₯,β„Ž,π‘š)   𝑅(β„Ž,π‘š)   𝐹(β„Ž,π‘š)   𝐺(β„Ž,π‘š)   𝐻(β„Ž,π‘š)   𝐼(π‘₯)   0 (π‘š)
Proof of Theorem mdegleb
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 mdegval.d . . . . 5 𝐷 = (𝐼 mDeg 𝑅)
2 mdegval.p . . . . 5 𝑃 = (𝐼 mPoly 𝑅)
3 mdegval.b . . . . 5 𝐡 = (Baseβ€˜π‘ƒ)
4 mdegval.z . . . . 5 0 = (0gβ€˜π‘…)
5 mdegval.a . . . . 5 𝐴 = {π‘š ∈ (β„•0 ↑m 𝐼) ∣ (β—‘π‘š β€œ β„•) ∈ Fin}
6 mdegval.h . . . . 5 𝐻 = (β„Ž ∈ 𝐴 ↦ (β„‚fld Ξ£g β„Ž))
71, 2, 3, 4, 5, 6mdegval 25816 . . . 4 (𝐹 ∈ 𝐡 β†’ (π·β€˜πΉ) = sup((𝐻 β€œ (𝐹 supp 0 )), ℝ*, < ))
87adantr 479 . . 3 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ (π·β€˜πΉ) = sup((𝐻 β€œ (𝐹 supp 0 )), ℝ*, < ))
98breq1d 5157 . 2 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ ((π·β€˜πΉ) ≀ 𝐺 ↔ sup((𝐻 β€œ (𝐹 supp 0 )), ℝ*, < ) ≀ 𝐺))
10 imassrn 6069 . . . 4 (𝐻 β€œ (𝐹 supp 0 )) βŠ† ran 𝐻
115, 6tdeglem1 25808 . . . . . . 7 𝐻:π΄βŸΆβ„•0
1211a1i 11 . . . . . 6 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ 𝐻:π΄βŸΆβ„•0)
1312frnd 6724 . . . . 5 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ ran 𝐻 βŠ† β„•0)
14 nn0ssre 12480 . . . . . 6 β„•0 βŠ† ℝ
15 ressxr 11262 . . . . . 6 ℝ βŠ† ℝ*
1614, 15sstri 3990 . . . . 5 β„•0 βŠ† ℝ*
1713, 16sstrdi 3993 . . . 4 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ ran 𝐻 βŠ† ℝ*)
1810, 17sstrid 3992 . . 3 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ (𝐻 β€œ (𝐹 supp 0 )) βŠ† ℝ*)
19 supxrleub 13309 . . 3 (((𝐻 β€œ (𝐹 supp 0 )) βŠ† ℝ* ∧ 𝐺 ∈ ℝ*) β†’ (sup((𝐻 β€œ (𝐹 supp 0 )), ℝ*, < ) ≀ 𝐺 ↔ βˆ€π‘¦ ∈ (𝐻 β€œ (𝐹 supp 0 ))𝑦 ≀ 𝐺))
2018, 19sylancom 586 . 2 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ (sup((𝐻 β€œ (𝐹 supp 0 )), ℝ*, < ) ≀ 𝐺 ↔ βˆ€π‘¦ ∈ (𝐻 β€œ (𝐹 supp 0 ))𝑦 ≀ 𝐺))
2112ffnd 6717 . . . 4 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ 𝐻 Fn 𝐴)
22 suppssdm 8164 . . . . 5 (𝐹 supp 0 ) βŠ† dom 𝐹
23 eqid 2730 . . . . . 6 (Baseβ€˜π‘…) = (Baseβ€˜π‘…)
24 simpl 481 . . . . . 6 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ 𝐹 ∈ 𝐡)
252, 23, 3, 5, 24mplelf 21776 . . . . 5 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ 𝐹:𝐴⟢(Baseβ€˜π‘…))
2622, 25fssdm 6736 . . . 4 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ (𝐹 supp 0 ) βŠ† 𝐴)
27 breq1 5150 . . . . 5 (𝑦 = (π»β€˜π‘₯) β†’ (𝑦 ≀ 𝐺 ↔ (π»β€˜π‘₯) ≀ 𝐺))
2827ralima 7241 . . . 4 ((𝐻 Fn 𝐴 ∧ (𝐹 supp 0 ) βŠ† 𝐴) β†’ (βˆ€π‘¦ ∈ (𝐻 β€œ (𝐹 supp 0 ))𝑦 ≀ 𝐺 ↔ βˆ€π‘₯ ∈ (𝐹 supp 0 )(π»β€˜π‘₯) ≀ 𝐺))
2921, 26, 28syl2anc 582 . . 3 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ (βˆ€π‘¦ ∈ (𝐻 β€œ (𝐹 supp 0 ))𝑦 ≀ 𝐺 ↔ βˆ€π‘₯ ∈ (𝐹 supp 0 )(π»β€˜π‘₯) ≀ 𝐺))
3025ffnd 6717 . . . . . . . 8 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ 𝐹 Fn 𝐴)
314fvexi 6904 . . . . . . . . 9 0 ∈ V
3231a1i 11 . . . . . . . 8 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ 0 ∈ V)
33 elsuppfng 8157 . . . . . . . 8 ((𝐹 Fn 𝐴 ∧ 𝐹 ∈ 𝐡 ∧ 0 ∈ V) β†’ (π‘₯ ∈ (𝐹 supp 0 ) ↔ (π‘₯ ∈ 𝐴 ∧ (πΉβ€˜π‘₯) β‰  0 )))
3430, 24, 32, 33syl3anc 1369 . . . . . . 7 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ (π‘₯ ∈ (𝐹 supp 0 ) ↔ (π‘₯ ∈ 𝐴 ∧ (πΉβ€˜π‘₯) β‰  0 )))
35 fvex 6903 . . . . . . . . . 10 (πΉβ€˜π‘₯) ∈ V
3635biantrur 529 . . . . . . . . 9 ((πΉβ€˜π‘₯) β‰  0 ↔ ((πΉβ€˜π‘₯) ∈ V ∧ (πΉβ€˜π‘₯) β‰  0 ))
37 eldifsn 4789 . . . . . . . . 9 ((πΉβ€˜π‘₯) ∈ (V βˆ– { 0 }) ↔ ((πΉβ€˜π‘₯) ∈ V ∧ (πΉβ€˜π‘₯) β‰  0 ))
3836, 37bitr4i 277 . . . . . . . 8 ((πΉβ€˜π‘₯) β‰  0 ↔ (πΉβ€˜π‘₯) ∈ (V βˆ– { 0 }))
3938anbi2i 621 . . . . . . 7 ((π‘₯ ∈ 𝐴 ∧ (πΉβ€˜π‘₯) β‰  0 ) ↔ (π‘₯ ∈ 𝐴 ∧ (πΉβ€˜π‘₯) ∈ (V βˆ– { 0 })))
4034, 39bitrdi 286 . . . . . 6 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ (π‘₯ ∈ (𝐹 supp 0 ) ↔ (π‘₯ ∈ 𝐴 ∧ (πΉβ€˜π‘₯) ∈ (V βˆ– { 0 }))))
4140imbi1d 340 . . . . 5 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ ((π‘₯ ∈ (𝐹 supp 0 ) β†’ (π»β€˜π‘₯) ≀ 𝐺) ↔ ((π‘₯ ∈ 𝐴 ∧ (πΉβ€˜π‘₯) ∈ (V βˆ– { 0 })) β†’ (π»β€˜π‘₯) ≀ 𝐺)))
42 impexp 449 . . . . . 6 (((π‘₯ ∈ 𝐴 ∧ (πΉβ€˜π‘₯) ∈ (V βˆ– { 0 })) β†’ (π»β€˜π‘₯) ≀ 𝐺) ↔ (π‘₯ ∈ 𝐴 β†’ ((πΉβ€˜π‘₯) ∈ (V βˆ– { 0 }) β†’ (π»β€˜π‘₯) ≀ 𝐺)))
43 con34b 315 . . . . . . . 8 (((πΉβ€˜π‘₯) ∈ (V βˆ– { 0 }) β†’ (π»β€˜π‘₯) ≀ 𝐺) ↔ (Β¬ (π»β€˜π‘₯) ≀ 𝐺 β†’ Β¬ (πΉβ€˜π‘₯) ∈ (V βˆ– { 0 })))
44 simplr 765 . . . . . . . . . . 11 (((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) ∧ π‘₯ ∈ 𝐴) β†’ 𝐺 ∈ ℝ*)
4512ffvelcdmda 7085 . . . . . . . . . . . 12 (((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) ∧ π‘₯ ∈ 𝐴) β†’ (π»β€˜π‘₯) ∈ β„•0)
4616, 45sselid 3979 . . . . . . . . . . 11 (((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) ∧ π‘₯ ∈ 𝐴) β†’ (π»β€˜π‘₯) ∈ ℝ*)
47 xrltnle 11285 . . . . . . . . . . 11 ((𝐺 ∈ ℝ* ∧ (π»β€˜π‘₯) ∈ ℝ*) β†’ (𝐺 < (π»β€˜π‘₯) ↔ Β¬ (π»β€˜π‘₯) ≀ 𝐺))
4844, 46, 47syl2anc 582 . . . . . . . . . 10 (((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) ∧ π‘₯ ∈ 𝐴) β†’ (𝐺 < (π»β€˜π‘₯) ↔ Β¬ (π»β€˜π‘₯) ≀ 𝐺))
4948bicomd 222 . . . . . . . . 9 (((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) ∧ π‘₯ ∈ 𝐴) β†’ (Β¬ (π»β€˜π‘₯) ≀ 𝐺 ↔ 𝐺 < (π»β€˜π‘₯)))
50 ianor 978 . . . . . . . . . . 11 (Β¬ ((πΉβ€˜π‘₯) ∈ V ∧ (πΉβ€˜π‘₯) β‰  0 ) ↔ (Β¬ (πΉβ€˜π‘₯) ∈ V ∨ Β¬ (πΉβ€˜π‘₯) β‰  0 ))
5150, 37xchnxbir 332 . . . . . . . . . 10 (Β¬ (πΉβ€˜π‘₯) ∈ (V βˆ– { 0 }) ↔ (Β¬ (πΉβ€˜π‘₯) ∈ V ∨ Β¬ (πΉβ€˜π‘₯) β‰  0 ))
52 orcom 866 . . . . . . . . . . . 12 ((Β¬ (πΉβ€˜π‘₯) ∈ V ∨ Β¬ (πΉβ€˜π‘₯) β‰  0 ) ↔ (Β¬ (πΉβ€˜π‘₯) β‰  0 ∨ Β¬ (πΉβ€˜π‘₯) ∈ V))
5335notnoti 143 . . . . . . . . . . . . 13 Β¬ Β¬ (πΉβ€˜π‘₯) ∈ V
5453biorfi 935 . . . . . . . . . . . 12 (Β¬ (πΉβ€˜π‘₯) β‰  0 ↔ (Β¬ (πΉβ€˜π‘₯) β‰  0 ∨ Β¬ (πΉβ€˜π‘₯) ∈ V))
55 nne 2942 . . . . . . . . . . . 12 (Β¬ (πΉβ€˜π‘₯) β‰  0 ↔ (πΉβ€˜π‘₯) = 0 )
5652, 54, 553bitr2i 298 . . . . . . . . . . 11 ((Β¬ (πΉβ€˜π‘₯) ∈ V ∨ Β¬ (πΉβ€˜π‘₯) β‰  0 ) ↔ (πΉβ€˜π‘₯) = 0 )
5756a1i 11 . . . . . . . . . 10 (((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) ∧ π‘₯ ∈ 𝐴) β†’ ((Β¬ (πΉβ€˜π‘₯) ∈ V ∨ Β¬ (πΉβ€˜π‘₯) β‰  0 ) ↔ (πΉβ€˜π‘₯) = 0 ))
5851, 57bitrid 282 . . . . . . . . 9 (((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) ∧ π‘₯ ∈ 𝐴) β†’ (Β¬ (πΉβ€˜π‘₯) ∈ (V βˆ– { 0 }) ↔ (πΉβ€˜π‘₯) = 0 ))
5949, 58imbi12d 343 . . . . . . . 8 (((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) ∧ π‘₯ ∈ 𝐴) β†’ ((Β¬ (π»β€˜π‘₯) ≀ 𝐺 β†’ Β¬ (πΉβ€˜π‘₯) ∈ (V βˆ– { 0 })) ↔ (𝐺 < (π»β€˜π‘₯) β†’ (πΉβ€˜π‘₯) = 0 )))
6043, 59bitrid 282 . . . . . . 7 (((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) ∧ π‘₯ ∈ 𝐴) β†’ (((πΉβ€˜π‘₯) ∈ (V βˆ– { 0 }) β†’ (π»β€˜π‘₯) ≀ 𝐺) ↔ (𝐺 < (π»β€˜π‘₯) β†’ (πΉβ€˜π‘₯) = 0 )))
6160pm5.74da 800 . . . . . 6 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ ((π‘₯ ∈ 𝐴 β†’ ((πΉβ€˜π‘₯) ∈ (V βˆ– { 0 }) β†’ (π»β€˜π‘₯) ≀ 𝐺)) ↔ (π‘₯ ∈ 𝐴 β†’ (𝐺 < (π»β€˜π‘₯) β†’ (πΉβ€˜π‘₯) = 0 ))))
6242, 61bitrid 282 . . . . 5 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ (((π‘₯ ∈ 𝐴 ∧ (πΉβ€˜π‘₯) ∈ (V βˆ– { 0 })) β†’ (π»β€˜π‘₯) ≀ 𝐺) ↔ (π‘₯ ∈ 𝐴 β†’ (𝐺 < (π»β€˜π‘₯) β†’ (πΉβ€˜π‘₯) = 0 ))))
6341, 62bitrd 278 . . . 4 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ ((π‘₯ ∈ (𝐹 supp 0 ) β†’ (π»β€˜π‘₯) ≀ 𝐺) ↔ (π‘₯ ∈ 𝐴 β†’ (𝐺 < (π»β€˜π‘₯) β†’ (πΉβ€˜π‘₯) = 0 ))))
6463ralbidv2 3171 . . 3 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ (βˆ€π‘₯ ∈ (𝐹 supp 0 )(π»β€˜π‘₯) ≀ 𝐺 ↔ βˆ€π‘₯ ∈ 𝐴 (𝐺 < (π»β€˜π‘₯) β†’ (πΉβ€˜π‘₯) = 0 )))
6529, 64bitrd 278 . 2 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ (βˆ€π‘¦ ∈ (𝐻 β€œ (𝐹 supp 0 ))𝑦 ≀ 𝐺 ↔ βˆ€π‘₯ ∈ 𝐴 (𝐺 < (π»β€˜π‘₯) β†’ (πΉβ€˜π‘₯) = 0 )))
669, 20, 653bitrd 304 1 ((𝐹 ∈ 𝐡 ∧ 𝐺 ∈ ℝ*) β†’ ((π·β€˜πΉ) ≀ 𝐺 ↔ βˆ€π‘₯ ∈ 𝐴 (𝐺 < (π»β€˜π‘₯) β†’ (πΉβ€˜π‘₯) = 0 )))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 843   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  {crab 3430  Vcvv 3472   βˆ– cdif 3944   βŠ† wss 3947  {csn 4627   class class class wbr 5147   ↦ cmpt 5230  β—‘ccnv 5674  ran crn 5676   β€œ cima 5678   Fn wfn 6537  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411   supp csupp 8148   ↑m cmap 8822  Fincfn 8941  supcsup 9437  β„cr 11111  β„*cxr 11251   < clt 11252   ≀ cle 11253  β„•cn 12216  β„•0cn0 12476  Basecbs 17148  0gc0g 17389   Ξ£g cgsu 17390  β„‚fldccnfld 21144   mPoly cmpl 21678   mDeg cmdg 25803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191  ax-mulf 11192
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-sup 9439  df-oi 9507  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-fz 13489  df-fzo 13632  df-seq 13971  df-hash 14295  df-struct 17084  df-sets 17101  df-slot 17119  df-ndx 17131  df-base 17149  df-ress 17178  df-plusg 17214  df-mulr 17215  df-starv 17216  df-sca 17217  df-vsca 17218  df-tset 17220  df-ple 17221  df-ds 17223  df-unif 17224  df-0g 17391  df-gsum 17392  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-submnd 18706  df-grp 18858  df-minusg 18859  df-cntz 19222  df-cmn 19691  df-abl 19692  df-mgp 20029  df-ur 20076  df-ring 20129  df-cring 20130  df-cnfld 21145  df-psr 21681  df-mpl 21683  df-mdeg 25805
This theorem is referenced by:  mdeglt  25818  mdegaddle  25827  mdegvscale  25828  mdegle0  25830  mdegmullem  25831  deg1leb  25848
  Copyright terms: Public domain W3C validator