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 ‘ 𝑅 )
	isnzr.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	nzrnz	⊢ ( 𝑅 ∈ NzRing → 1 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		isnzr.o	⊢ 1 = ( 1r ‘ 𝑅 )
2		isnzr.z	⊢ 0 = ( 0g ‘ 𝑅 )
3	1 2	isnzr	⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) )
4	3	simprbi	⊢ ( 𝑅 ∈ NzRing → 1 ≠ 0 )