Theorem nzrunit

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

	Ref	Expression
Hypotheses	nzrunit.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	nzrunit.2	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	nzrunit	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		nzrunit.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
2		nzrunit.2	⊢ 0 = ( 0g ‘ 𝑅 )
3		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
4	3 2	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ 0 )
5		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
6	1 2 3	0unit	⊢ ( 𝑅 ∈ Ring → ( 0 ∈ 𝑈 ↔ ( 1r ‘ 𝑅 ) = 0 ) )
7	6	necon3bbid	⊢ ( 𝑅 ∈ Ring → ( ¬ 0 ∈ 𝑈 ↔ ( 1r ‘ 𝑅 ) ≠ 0 ) )
8	5 7	syl	⊢ ( 𝑅 ∈ NzRing → ( ¬ 0 ∈ 𝑈 ↔ ( 1r ‘ 𝑅 ) ≠ 0 ) )
9	4 8	mpbird	⊢ ( 𝑅 ∈ NzRing → ¬ 0 ∈ 𝑈 )
10		eleq1	⊢ ( 𝐴 = 0 → ( 𝐴 ∈ 𝑈 ↔ 0 ∈ 𝑈 ) )
11	10	notbid	⊢ ( 𝐴 = 0 → ( ¬ 𝐴 ∈ 𝑈 ↔ ¬ 0 ∈ 𝑈 ) )
12	9 11	syl5ibrcom	⊢ ( 𝑅 ∈ NzRing → ( 𝐴 = 0 → ¬ 𝐴 ∈ 𝑈 ) )
13	12	necon2ad	⊢ ( 𝑅 ∈ NzRing → ( 𝐴 ∈ 𝑈 → 𝐴 ≠ 0 ) )
14	13	imp	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ≠ 0 )