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

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 = \deg_{1} (R)$
	deg1z.p	$⊢ P = {Poly}_{1} (R)$
	deg1z.z	$⊢ \underset{˙}{0} = 0_{P}$
	deg1nn0cl.b	$⊢ B = {Base}_{P}$
Assertion	deg1nn0cl	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to D (F) \in ℕ_{0}$

Step	Hyp	Ref	Expression
1		deg1z.d	$⊢ D = \deg_{1} (R)$
2		deg1z.p	$⊢ P = {Poly}_{1} (R)$
3		deg1z.z	$⊢ \underset{˙}{0} = 0_{P}$
4		deg1nn0cl.b	$⊢ B = {Base}_{P}$
5	1	deg1fval	$⊢ D = 1_{𝑜} mDeg R$
6		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
7	6 2 3	ply1mpl0	$⊢ \underset{˙}{0} = 0_{(1_{𝑜} mPoly R)}$
8	2 4	ply1bas	$⊢ B = {Base}_{(1_{𝑜} mPoly R)}$
9	5 6 7 8	mdegnn0cl	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to D (F) \in ℕ_{0}$