Definition df-dgr

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

	Ref	Expression
Assertion	df-dgr	|- deg = ( f e. ( Poly ` CC ) |-> sup ( ( `' ( coeff ` f ) " ( CC \ { 0 } ) ) , NN0 , < ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdgr	|- deg
1		vf	|- f
2		cply	|- Poly
3		cc	|- CC
4	3 2	cfv	|- ( Poly ` CC )
5		ccoe	|- coeff
6	1	cv	|- f
7	6 5	cfv	|- ( coeff ` f )
8	7	ccnv	|- `' ( coeff ` f )
9		cc0	|- 0
10	9	csn	|- { 0 }
11	3 10	cdif	|- ( CC \ { 0 } )
12	8 11	cima	|- ( `' ( coeff ` f ) " ( CC \ { 0 } ) )
13		cn0	|- NN0
14		clt	|- <
15	12 13 14	csup	|- sup ( ( `' ( coeff ` f ) " ( CC \ { 0 } ) ) , NN0 , < )
16	1 4 15	cmpt	|- ( f e. ( Poly ` CC ) |-> sup ( ( `' ( coeff ` f ) " ( CC \ { 0 } ) ) , NN0 , < ) )
17	0 16	wceq	|- deg = ( f e. ( Poly ` CC ) |-> sup ( ( `' ( coeff ` f ) " ( CC \ { 0 } ) ) , NN0 , < ) )