Theorem zringnzr

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

	Ref	Expression
Assertion	zringnzr	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{NzRing}$$

Proof

Step	Hyp	Ref	Expression
1		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
2		ax-1ne0	$$⊢1\ne 0$$
3		zring1	$$⊢1=1_{{\mathbb{Z}}_{\mathrm{ring}}}$$
4		zring0	$$⊢0=0_{{\mathbb{Z}}_{\mathrm{ring}}}$$
5	3 4	isnzr	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{NzRing}\leftrightarrow \left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\wedge 1\ne 0\right)$$
6	1 2 5	mpbir2an	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{NzRing}$$