Theorem nzrnz

Description: One and zero are different in a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015)

	Ref	Expression
Hypotheses	isnzr.o	|- .1. = ( 1r ` R )
	isnzr.z	|- .0. = ( 0g ` R )
Assertion	nzrnz	|- ( R e. NzRing -> .1. =/= .0. )

Proof

Step	Hyp	Ref	Expression
1		isnzr.o	|- .1. = ( 1r ` R )
2		isnzr.z	|- .0. = ( 0g ` R )
3	1 2	isnzr	|- ( R e. NzRing <-> ( R e. Ring /\ .1. =/= .0. ) )
4	3	simprbi	|- ( R e. NzRing -> .1. =/= .0. )