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	$$⊢\underset{\dot{}}{0}=0_R$$
	zrdrng.1	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	zrdrng	$$⊢\underset{\dot{}}{0}=\underset{\dot{}}{1}\to \neg R\in \mathrm{DivRing}$$

Proof

Step	Hyp	Ref	Expression
1		zrdrng.0	$$⊢\underset{\dot{}}{0}=0_R$$
2		zrdrng.1	$$⊢\underset{\dot{}}{1}=1_R$$
3	1 2	drngunz	$$⊢R\in \mathrm{DivRing}\to \underset{\dot{}}{1}\ne \underset{\dot{}}{0}$$
4	3	necomd	$$⊢R\in \mathrm{DivRing}\to \underset{\dot{}}{0}\ne \underset{\dot{}}{1}$$
5	4	necon2bi	$$⊢\underset{\dot{}}{0}=\underset{\dot{}}{1}\to \neg R\in \mathrm{DivRing}$$