Theorem zringnzr

Description: The ring of integers is a nonzero ring. (Contributed by AV, 18-Apr-2020)

	Ref	Expression
Assertion	zringnzr	⊢ ℤring ∈ NzRing

Proof

Step	Hyp	Ref	Expression
1		zringring	⊢ ℤring ∈ Ring
2		ax-1ne0	⊢ 1 ≠ 0
3		zring1	⊢ 1 = ( 1r ‘ ℤring )
4		zring0	⊢ 0 = ( 0g ‘ ℤring )
5	3 4	isnzr	⊢ ( ℤring ∈ NzRing ↔ ( ℤring ∈ Ring ∧ 1 ≠ 0 ) )
6	1 2 5	mpbir2an	⊢ ℤring ∈ NzRing