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	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
2	1	uztrn2	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ℕ )