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 23928
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 23924 . 2 class deg
2 vf . . 3 setvar 𝑓
3 cc 9919 . . . 4 class
4 cply 23921 . . . 4 class Poly
53, 4cfv 5876 . . 3 class (Poly‘ℂ)
62cv 1480 . . . . . . 7 class 𝑓
7 ccoe 23923 . . . . . . 7 class coeff
86, 7cfv 5876 . . . . . 6 class (coeff‘𝑓)
98ccnv 5103 . . . . 5 class (coeff‘𝑓)
10 cc0 9921 . . . . . . 7 class 0
1110csn 4168 . . . . . 6 class {0}
123, 11cdif 3564 . . . . 5 class (ℂ ∖ {0})
139, 12cima 5107 . . . 4 class ((coeff‘𝑓) “ (ℂ ∖ {0}))
14 cn0 11277 . . . 4 class 0
15 clt 10059 . . . 4 class <
1613, 14, 15csup 8331 . . 3 class sup(((coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < )
172, 5, 16cmpt 4720 . 2 class (𝑓 ∈ (Poly‘ℂ) ↦ sup(((coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < ))
181, 17wceq 1481 1 wff deg = (𝑓 ∈ (Poly‘ℂ) ↦ sup(((coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < ))
Colors of variables: wff setvar class
This definition is referenced by:  dgrval  23965
  Copyright terms: Public domain W3C validator