df-dgr

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

		Ref	Expression
	Assertion	df-dgr	$⊢ \deg = (f \in Poly (ℂ) ⟼ sup ({coeff (f)}^{-1} [ℂ ∖ \{0\}] ℕ_{0} <))$

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

Metamath Proof Explorer