Theorem dgrcl

Description: The degree of any polynomial is a nonnegative integer. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Assertion	dgrcl	|- ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( coeff ` F ) = ( coeff ` F )
2	1	dgrval	|- ( F e. ( Poly ` S ) -> ( deg ` F ) = sup ( ( `' ( coeff ` F ) " ( CC \ { 0 } ) ) , NN0 , < ) )
3		nn0ssre	|- NN0 C_ RR
4		ltso	|- < Or RR
5		soss	|- ( NN0 C_ RR -> ( < Or RR -> < Or NN0 ) )
6	3 4 5	mp2	|- < Or NN0
7	6	a1i	|- ( F e. ( Poly ` S ) -> < Or NN0 )
8		0zd	|- ( F e. ( Poly ` S ) -> 0 e. ZZ )
9		cnvimass	|- ( `' ( coeff ` F ) " ( CC \ { 0 } ) ) C_ dom ( coeff ` F )
10	1	coef	|- ( F e. ( Poly ` S ) -> ( coeff ` F ) : NN0 --> ( S u. { 0 } ) )
11	9 10	fssdm	|- ( F e. ( Poly ` S ) -> ( `' ( coeff ` F ) " ( CC \ { 0 } ) ) C_ NN0 )
12	1	dgrlem	|- ( F e. ( Poly ` S ) -> ( ( coeff ` F ) : NN0 --> ( S u. { 0 } ) /\ E. n e. ZZ A. x e. ( `' ( coeff ` F ) " ( CC \ { 0 } ) ) x <_ n ) )
13	12	simprd	|- ( F e. ( Poly ` S ) -> E. n e. ZZ A. x e. ( `' ( coeff ` F ) " ( CC \ { 0 } ) ) x <_ n )
14		nn0uz	|- NN0 = ( ZZ>= ` 0 )
15	14	uzsupss	|- ( ( 0 e. ZZ /\ ( `' ( coeff ` F ) " ( CC \ { 0 } ) ) C_ NN0 /\ E. n e. ZZ A. x e. ( `' ( coeff ` F ) " ( CC \ { 0 } ) ) x <_ n ) -> E. n e. NN0 ( A. x e. ( `' ( coeff ` F ) " ( CC \ { 0 } ) ) -. n < x /\ A. x e. NN0 ( x < n -> E. y e. ( `' ( coeff ` F ) " ( CC \ { 0 } ) ) x < y ) ) )
16	8 11 13 15	syl3anc	|- ( F e. ( Poly ` S ) -> E. n e. NN0 ( A. x e. ( `' ( coeff ` F ) " ( CC \ { 0 } ) ) -. n < x /\ A. x e. NN0 ( x < n -> E. y e. ( `' ( coeff ` F ) " ( CC \ { 0 } ) ) x < y ) ) )
17	7 16	supcl	|- ( F e. ( Poly ` S ) -> sup ( ( `' ( coeff ` F ) " ( CC \ { 0 } ) ) , NN0 , < ) e. NN0 )
18	2 17	eqeltrd	|- ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )