Theorem eluznn

Description: Membership in a positive upper set of integers implies membership in NN . (Contributed by JJ, 1-Oct-2018)

	Ref	Expression
Assertion	eluznn	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{Z}}_{\ge N}\right)\to M\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
2	1	uztrn2	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{Z}}_{\ge N}\right)\to M\in \mathbb{N}$$