MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dgr Structured version   Visualization version   GIF version

Definition df-dgr 24067
Description: Define the degree of a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.)
Assertion
Ref Expression
df-dgr deg = (𝑓 ∈ (Poly‘ℂ) ↦ sup(((coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < ))

Detailed syntax breakdown of Definition df-dgr
StepHypRef Expression
1 cdgr 24063 . 2 class deg
2 vf . . 3 setvar 𝑓
3 cc 10047 . . . 4 class
4 cply 24060 . . . 4 class Poly
53, 4cfv 6001 . . 3 class (Poly‘ℂ)
62cv 1595 . . . . . . 7 class 𝑓
7 ccoe 24062 . . . . . . 7 class coeff
86, 7cfv 6001 . . . . . 6 class (coeff‘𝑓)
98ccnv 5217 . . . . 5 class (coeff‘𝑓)
10 cc0 10049 . . . . . . 7 class 0
1110csn 4285 . . . . . 6 class {0}
123, 11cdif 3677 . . . . 5 class (ℂ ∖ {0})
139, 12cima 5221 . . . 4 class ((coeff‘𝑓) “ (ℂ ∖ {0}))
14 cn0 11405 . . . 4 class 0
15 clt 10187 . . . 4 class <
1613, 14, 15csup 8462 . . 3 class sup(((coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < )
172, 5, 16cmpt 4837 . 2 class (𝑓 ∈ (Poly‘ℂ) ↦ sup(((coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < ))
181, 17wceq 1596 1 wff deg = (𝑓 ∈ (Poly‘ℂ) ↦ sup(((coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < ))
Colors of variables: wff setvar class
This definition is referenced by:  dgrval  24104
  Copyright terms: Public domain W3C validator