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

Definition df-dgr 24892
 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 24888 . 2 class deg
2 vf . . 3 setvar 𝑓
3 cc 10578 . . . 4 class
4 cply 24885 . . . 4 class Poly
53, 4cfv 6339 . . 3 class (Poly‘ℂ)
62cv 1537 . . . . . . 7 class 𝑓
7 ccoe 24887 . . . . . . 7 class coeff
86, 7cfv 6339 . . . . . 6 class (coeff‘𝑓)
98ccnv 5526 . . . . 5 class (coeff‘𝑓)
10 cc0 10580 . . . . . . 7 class 0
1110csn 4525 . . . . . 6 class {0}
123, 11cdif 3857 . . . . 5 class (ℂ ∖ {0})
139, 12cima 5530 . . . 4 class ((coeff‘𝑓) “ (ℂ ∖ {0}))
14 cn0 11939 . . . 4 class 0
15 clt 10718 . . . 4 class <
1613, 14, 15csup 8942 . . 3 class sup(((coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < )
172, 5, 16cmpt 5115 . 2 class (𝑓 ∈ (Poly‘ℂ) ↦ sup(((coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < ))
181, 17wceq 1538 1 wff deg = (𝑓 ∈ (Poly‘ℂ) ↦ sup(((coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < ))
 Colors of variables: wff setvar class This definition is referenced by:  dgrval  24929
 Copyright terms: Public domain W3C validator