Definition df-dgr

Description: Define the degree of a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Assertion	df-dgr	$$⊢\mathrm{deg}=\left(f\in \mathrm{Poly}\left(ℂ\right)⟼sup\left({\mathrm{coeff}\left(f\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right],{\mathbb{N}}_0,<\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdgr	$$class\mathrm{deg}$$
1		vf	$$setvarf$$
2		cply	$$class\mathrm{Poly}$$
3		cc	$$classℂ$$
4	3 2	cfv	$$class\mathrm{Poly}\left(ℂ\right)$$
5		ccoe	$$class\mathrm{coeff}$$
6	1	cv	$$setvarf$$
7	6 5	cfv	$$class\mathrm{coeff}\left(f\right)$$
8	7	ccnv	$$class{\mathrm{coeff}\left(f\right)}^{-1}$$
9		cc0	$$class0$$
10	9	csn	$$class\left\{0\right\}$$
11	3 10	cdif	$$class\left(ℂ\setminus \left\{0\right\}\right)$$
12	8 11	cima	$$class{\mathrm{coeff}\left(f\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
13		cn0	$$class{\mathbb{N}}_0$$
14		clt	$$class<$$
15	12 13 14	csup	$$classsup\left({\mathrm{coeff}\left(f\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right],{\mathbb{N}}_0,<\right)$$
16	1 4 15	cmpt	$$class\left(f\in \mathrm{Poly}\left(ℂ\right)⟼sup\left({\mathrm{coeff}\left(f\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right],{\mathbb{N}}_0,<\right)\right)$$
17	0 16	wceq	$$wff\mathrm{deg}=\left(f\in \mathrm{Poly}\left(ℂ\right)⟼sup\left({\mathrm{coeff}\left(f\right)}^{-1}\left[ℂ\setminus \left\{0\right\}\right],{\mathbb{N}}_0,<\right)\right)$$