This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )