Theorem zrdrng

Description: A zero ring is not a division ring. (Contributed by FL, 24-Jan-2010) (Revised by AV, 22-Jul-2026)

	Ref	Expression
Hypotheses	zrdrng.0	⊢ 0 = ( 0g ‘ 𝑅 )
	zrdrng.1	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	zrdrng	⊢ ( 0 = 1 → ¬ 𝑅 ∈ DivRing )

Proof

Step	Hyp	Ref	Expression
1		zrdrng.0	⊢ 0 = ( 0g ‘ 𝑅 )
2		zrdrng.1	⊢ 1 = ( 1r ‘ 𝑅 )
3	1 2	drngunz	⊢ ( 𝑅 ∈ DivRing → 1 ≠ 0 )
4	3	necomd	⊢ ( 𝑅 ∈ DivRing → 0 ≠ 1 )
5	4	necon2bi	⊢ ( 0 = 1 → ¬ 𝑅 ∈ DivRing )