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 23665
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 23661 . 2 class deg
2 vf . . 3 setvar 𝑓
3 cc 9787 . . . 4 class
4 cply 23658 . . . 4 class Poly
53, 4cfv 5787 . . 3 class (Poly‘ℂ)
62cv 1473 . . . . . . 7 class 𝑓
7 ccoe 23660 . . . . . . 7 class coeff
86, 7cfv 5787 . . . . . 6 class (coeff‘𝑓)
98ccnv 5024 . . . . 5 class (coeff‘𝑓)
10 cc0 9789 . . . . . . 7 class 0
1110csn 4121 . . . . . 6 class {0}
123, 11cdif 3533 . . . . 5 class (ℂ ∖ {0})
139, 12cima 5028 . . . 4 class ((coeff‘𝑓) “ (ℂ ∖ {0}))
14 cn0 11136 . . . 4 class 0
15 clt 9927 . . . 4 class <
1613, 14, 15csup 8203 . . 3 class sup(((coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < )
172, 5, 16cmpt 4634 . 2 class (𝑓 ∈ (Poly‘ℂ) ↦ sup(((coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < ))
181, 17wceq 1474 1 wff deg = (𝑓 ∈ (Poly‘ℂ) ↦ sup(((coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < ))
Colors of variables: wff setvar class
This definition is referenced by:  dgrval  23702
  Copyright terms: Public domain W3C validator