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

Metamath Proof Explorer

Theorem mon1pn0

Description: Monic 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		mon1pn0.m	$⊢ M = {Monic}_{1p} (R)$
4		eqid	$⊢ {Base}_{P} = {Base}_{P}$
5		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
6		eqid	$⊢ 1_{R} = 1_{R}$
7	1 4 2 5 3 6	ismon1p	$⊢ F \in M \leftrightarrow (F \in {Base}_{P} \land F \neq \underset{˙}{0} \land {coe}_{1} (F) (\deg_{1} (R) (F)) = 1_{R})$
8	7	simp2bi	$⊢ F \in M \to F \neq \underset{˙}{0}$