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

Metamath Proof Explorer

Theorem uc1pn0

Description: Unitic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015)

Step	Hyp	Ref	Expression
1		uc1pn0.p	$⊢ P = {Poly}_{1} (R)$
2		uc1pn0.z	$⊢ \underset{˙}{0} = 0_{P}$
3		uc1pn0.c	$⊢ C = {Unic}_{1p} (R)$
4		eqid	$⊢ {Base}_{P} = {Base}_{P}$
5		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
6		eqid	$⊢ Unit (R) = Unit (R)$
7	1 4 2 5 3 6	isuc1p	$⊢ F \in C \leftrightarrow (F \in {Base}_{P} \land F \neq \underset{˙}{0} \land {coe}_{1} (F) (\deg_{1} (R) (F)) \in Unit (R))$
8	7	simp2bi	$⊢ F \in C \to F \neq \underset{˙}{0}$