Theorem uc1pdeg

Description: Unitic polynomials have nonnegative degrees. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	uc1pdeg.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	uc1pdeg.c	$$⊢C={Unic}_{\mathrm{1p}}\left(R\right)$$
Assertion	uc1pdeg	$$⊢\left(R\in \mathrm{Ring}\wedge F\in C\right)\to D\left(F\right)\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		uc1pdeg.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		uc1pdeg.c	$$⊢C={Unic}_{\mathrm{1p}}\left(R\right)$$
3		simpl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in C\right)\to R\in \mathrm{Ring}$$
4		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
5		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
6	4 5 2	uc1pcl	$$⊢F\in C\to F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
7	6	adantl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in C\right)\to F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
8		eqid	$$⊢0_{{\mathrm{Poly}}_1\left(R\right)}=0_{{\mathrm{Poly}}_1\left(R\right)}$$
9	4 8 2	uc1pn0	$$⊢F\in C\to F\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
10	9	adantl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in C\right)\to F\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
11	1 4 8 5	deg1nn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge F\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\right)\to D\left(F\right)\in {\mathbb{N}}_0$$
12	3 7 10 11	syl3anc	$$⊢\left(R\in \mathrm{Ring}\wedge F\in C\right)\to D\left(F\right)\in {\mathbb{N}}_0$$