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={\mathrm{deg}}_1\left(R\right)$$
	deg1z.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	deg1z.z	$$⊢\underset{\dot{}}{0}=0_P$$
	deg1nn0cl.b	$$⊢B={\mathrm{Base}}_P$$
Assertion	deg1nn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to D\left(F\right)\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		deg1z.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		deg1z.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		deg1z.z	$$⊢\underset{\dot{}}{0}=0_P$$
4		deg1nn0cl.b	$$⊢B={\mathrm{Base}}_P$$
5	1	deg1fval	$$⊢D=1_{𝑜}\mathrm{mDeg}R$$
6		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
7	6 2 3	ply1mpl0	$$⊢\underset{\dot{}}{0}=0_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
8	2 4	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
9	5 6 7 8	mdegnn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to D\left(F\right)\in {\mathbb{N}}_0$$