Definition df-dgr 23947

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

Assertion

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

Detailed syntax breakdown of Definition df-dgr

Step	Hyp	Ref	Expression
1		cdgr 23943	. 2 class deg
2		vf	. . 3 setvar f
3		cc 9934	. . . 4 class CC
4		cply 23940	. . . 4 class Poly
5	3, 4	cfv 5888	. . 3 class (Poly ` CC )
6	2	cv 1482	. . . . . . 7 class f
7		ccoe 23942	. . . . . . 7 class coeff
8	6, 7	cfv 5888	. . . . . 6 class (coeff ` f )
9	8	ccnv 5113	. . . . 5 class `' (coeff ` f )
10		cc0 9936	. . . . . . 7 class 0
11	10	csn 4177	. . . . . 6 class { 0 }
12	3, 11	cdif 3571	. . . . 5 class ( CC \ { 0 } )
13	9, 12	cima 5117	. . . 4 class ( `' (coeff ` f ) " ( CC \ { 0 } ) )
14		cn0 11292	. . . 4 class NN0
15		clt 10074	. . . 4 class <
16	13, 14, 15	csup 8346	. . 3 class sup ( ( `' (coeff ` f ) " ( CC \ { 0 } ) ) , NN0 , < )
17	2, 5, 16	cmpt 4729	. 2 class ( f e. (Poly ` CC ) |-> sup ( ( `' (coeff ` f ) " ( CC \ { 0 } ) ) , NN0 , < ) )
18	1, 17	wceq 1483	1 wff deg = ( f e. (Poly ` CC ) |-> sup ( ( `' (coeff ` f ) " ( CC \ { 0 } ) ) , NN0 , < ) )

This definition is referenced by:  dgrval  23984