Metamath Proof Explorer

Theorem deg1nn0cl

Description: Degree of a nonzero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses deg1z.d 
|- D = ( deg1 ` R )
deg1z.p 
|- P = ( Poly1 ` R )
deg1z.z 
|- .0. = ( 0g ` P )
deg1nn0cl.b 
|- B = ( Base ` P )
Assertion deg1nn0cl 
|- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 )

Proof

Step Hyp Ref Expression
1 deg1z.d 
 |-  D = ( deg1 ` R )
2 deg1z.p 
 |-  P = ( Poly1 ` R )
3 deg1z.z 
 |-  .0. = ( 0g ` P )
4 deg1nn0cl.b 
 |-  B = ( Base ` P )
5 1 deg1fval 
 |-  D = ( 1o mDeg R )
6 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
7 6 2 3 ply1mpl0 
 |-  .0. = ( 0g ` ( 1o mPoly R ) )
8 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
9 2 8 4 ply1bas 
 |-  B = ( Base ` ( 1o mPoly R ) )
10 5 6 7 9 mdegnn0cl 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 )