Theorem eluz2nn

Description: An integer greater than or equal to 2 is a positive integer. (Contributed by AV, 3-Nov-2018)

	Ref	Expression
Assertion	eluz2nn	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		1z	$$⊢1\in \mathbb{Z}$$
2		1le2	$$⊢1\le 2$$
3		eluzuzle	$$⊢\left(1\in \mathbb{Z}\wedge 1\le 2\right)\to \left(A\in {\mathbb{Z}}_{\ge 2}\to A\in {\mathbb{Z}}_{\ge 1}\right)$$
4	1 2 3	mp2an	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in {\mathbb{Z}}_{\ge 1}$$
5		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
6	4 5	eleqtrrdi	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in \mathbb{N}$$