Definition df-dgr 24469

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

Step	Hyp	Ref	Expression
1		cdgr 24465	. 2 class deg
2		vf	. . 3 setvar 𝑓
3		cc 10386	. . . 4 class ℂ
4		cply 24462	. . . 4 class Poly
5	3, 4	cfv 6230	. . 3 class (Poly‘ℂ)
6	2	cv 1521	. . . . . . 7 class 𝑓
7		ccoe 24464	. . . . . . 7 class coeff
8	6, 7	cfv 6230	. . . . . 6 class (coeff‘𝑓)
9	8	ccnv 5447	. . . . 5 class ◡(coeff‘𝑓)
10		cc0 10388	. . . . . . 7 class 0
11	10	csn 4476	. . . . . 6 class {0}
12	3, 11	cdif 3860	. . . . 5 class (ℂ ∖ {0})
13	9, 12	cima 5451	. . . 4 class (◡(coeff‘𝑓) “ (ℂ ∖ {0}))
14		cn0 11750	. . . 4 class ℕ0
15		clt 10526	. . . 4 class <
16	13, 14, 15	csup 8755	. . 3 class sup((◡(coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < )
17	2, 5, 16	cmpt 5045	. 2 class (𝑓 ∈ (Poly‘ℂ) ↦ sup((◡(coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < ))
18	1, 17	wceq 1522	1 wff deg = (𝑓 ∈ (Poly‘ℂ) ↦ sup((◡(coeff‘𝑓) “ (ℂ ∖ {0})), ℕ0, < ))

This definition is referenced by:  dgrval  24506