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	2 4	ply1bas	|- B = ( Base ` ( 1o mPoly R ) )
9	5 6 7 8	mdegnn0cl	|- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 )