Theorem 0z

Description: Zero is an integer. (Contributed by NM, 12-Jan-2002)

	Ref	Expression
Assertion	0z	$$⊢0\in \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2		eqid	$$⊢0=0$$
3	2	3mix1i	$$⊢\left(0=0\vee 0\in \mathbb{N}\vee -0\in \mathbb{N}\right)$$
4		elz	$$⊢0\in \mathbb{Z}\leftrightarrow \left(0\in ℝ\wedge \left(0=0\vee 0\in \mathbb{N}\vee -0\in \mathbb{N}\right)\right)$$
5	1 3 4	mpbir2an	$$⊢0\in \mathbb{Z}$$