Theorem nzrunit

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

	Ref	Expression
Hypotheses	nzrunit.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
	nzrunit.2	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	nzrunit	$$⊢\left(R\in \mathrm{NzRing}\wedge A\in U\right)\to A\ne \underset{\dot{}}{0}$$

Proof

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