This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ \underset{˙}{1} = 1_{R}$
	isnzr.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	nzrnz	$⊢ R \in NzRing \to \underset{˙}{1} \neq \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		isnzr.o	$⊢ \underset{˙}{1} = 1_{R}$
2		isnzr.z	$⊢ \underset{˙}{0} = 0_{R}$
3	1 2	isnzr	$⊢ R \in NzRing \leftrightarrow (R \in Ring \land \underset{˙}{1} \neq \underset{˙}{0})$
4	3	simprbi	$⊢ R \in NzRing \to \underset{˙}{1} \neq \underset{˙}{0}$