Theorem eluznn0

Description: Membership in a nonnegative upper set of integers implies membership in NN0 . (Contributed by Paul Chapman, 22-Jun-2011)

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

Proof

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