uc1pdeg

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

Step	Hyp	Ref	Expression
1		uc1pdeg.d	$⊢ D = \deg_{1} (R)$
2		uc1pdeg.c	$⊢ C = {Unic}_{1p} (R)$
3		simpl	$⊢ (R \in Ring \land F \in C) \to R \in Ring$
4		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
5		eqid	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{{Poly}_{1} (R)}$
6	4 5 2	uc1pcl	$⊢ F \in C \to F \in {Base}_{{Poly}_{1} (R)}$
7	6	adantl	$⊢ (R \in Ring \land F \in C) \to F \in {Base}_{{Poly}_{1} (R)}$
8		eqid	$⊢ 0_{{Poly}_{1} (R)} = 0_{{Poly}_{1} (R)}$
9	4 8 2	uc1pn0	$⊢ F \in C \to F \neq 0_{{Poly}_{1} (R)}$
10	9	adantl	$⊢ (R \in Ring \land F \in C) \to F \neq 0_{{Poly}_{1} (R)}$
11	1 4 8 5	deg1nn0cl	$⊢ (R \in Ring \land F \in {Base}_{{Poly}_{1} (R)} \land F \neq 0_{{Poly}_{1} (R)}) \to D (F) \in ℕ_{0}$
12	3 7 10 11	syl3anc	$⊢ (R \in Ring \land F \in C) \to D (F) \in ℕ_{0}$

Metamath Proof Explorer