nzrunit

Description: A unit is nonzero in any nonzero ring. (Contributed by Mario Carneiro, 6-Oct-2015)

	Ref	Expression
Hypotheses	nzrunit.1	$⊢ U = Unit (R)$
	nzrunit.2	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	nzrunit	$⊢ (R \in NzRing \land A \in U) \to A \neq \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		nzrunit.1	$⊢ U = Unit (R)$
2		nzrunit.2	$⊢ \underset{˙}{0} = 0_{R}$
3		eqid	$⊢ 1_{R} = 1_{R}$
4	3 2	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq \underset{˙}{0}$
5		nzrring	$⊢ R \in NzRing \to R \in Ring$
6	1 2 3	0unit	$⊢ R \in Ring \to (\underset{˙}{0} \in U \leftrightarrow 1_{R} = \underset{˙}{0})$
7	6	necon3bbid	$⊢ R \in Ring \to (\neg \underset{˙}{0} \in U \leftrightarrow 1_{R} \neq \underset{˙}{0})$
8	5 7	syl	$⊢ R \in NzRing \to (\neg \underset{˙}{0} \in U \leftrightarrow 1_{R} \neq \underset{˙}{0})$
9	4 8	mpbird	$⊢ R \in NzRing \to \neg \underset{˙}{0} \in U$
10		eleq1	$⊢ A = \underset{˙}{0} \to (A \in U \leftrightarrow \underset{˙}{0} \in U)$
11	10	notbid	$⊢ A = \underset{˙}{0} \to (\neg A \in U \leftrightarrow \neg \underset{˙}{0} \in U)$
12	9 11	syl5ibrcom	$⊢ R \in NzRing \to (A = \underset{˙}{0} \to \neg A \in U)$
13	12	necon2ad	$⊢ R \in NzRing \to (A \in U \to A \neq \underset{˙}{0})$
14	13	imp	$⊢ (R \in NzRing \land A \in U) \to A \neq \underset{˙}{0}$

Metamath Proof Explorer