Theorem 1eluzge0

Description: 1 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018)

	Ref	Expression
Assertion	1eluzge0	$$⊢1\in {\mathbb{Z}}_{\ge 0}$$

Proof

Step	Hyp	Ref	Expression
1		0z	$$⊢0\in \mathbb{Z}$$
2		1z	$$⊢1\in \mathbb{Z}$$
3		0le1	$$⊢0\le 1$$
4		eluz2	$$⊢1\in {\mathbb{Z}}_{\ge 0}\leftrightarrow \left(0\in \mathbb{Z}\wedge 1\in \mathbb{Z}\wedge 0\le 1\right)$$
5	1 2 3 4	mpbir3an	$$⊢1\in {\mathbb{Z}}_{\ge 0}$$