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 ` R )
	zrdrng.1	|- .1. = ( 1r ` R )
Assertion	zrdrng	|- ( .0. = .1. -> -. R e. DivRing )

Proof

Step	Hyp	Ref	Expression
1		zrdrng.0	|- .0. = ( 0g ` R )
2		zrdrng.1	|- .1. = ( 1r ` R )
3	1 2	drngunz	|- ( R e. DivRing -> .1. =/= .0. )
4	3	necomd	|- ( R e. DivRing -> .0. =/= .1. )
5	4	necon2bi	|- ( .0. = .1. -> -. R e. DivRing )