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

Metamath Proof Explorer

Theorem 0z

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

		Ref	Expression
	Assertion	0z	$⊢ 0 \in ℤ$

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2		eqid	$⊢ 0 = 0$
3	2	3mix1i	$⊢ (0 = 0 \lor 0 \in ℕ \lor - 0 \in ℕ)$
4		elz	$⊢ 0 \in ℤ \leftrightarrow (0 \in ℝ \land (0 = 0 \lor 0 \in ℕ \lor - 0 \in ℕ))$
5	1 3 4	mpbir2an	$⊢ 0 \in ℤ$