Theorem drngnzr

Description: All division rings are nonzero. (Contributed by Stefan O'Rear, 24-Feb-2015)

	Ref	Expression
Assertion	drngnzr	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ NzRing )

Proof

Step	Hyp	Ref	Expression
1		drngring	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
2		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
3		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
4	2 3	drngunz	⊢ ( 𝑅 ∈ DivRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
5	3 2	isnzr	⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) )
6	1 4 5	sylanbrc	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ NzRing )