This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (N \in ℕ \land M \in ℤ_{\geq N}) \to M \in ℕ$

Step	Hyp	Ref	Expression
1		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
2	1	uztrn2	$⊢ (N \in ℕ \land M \in ℤ_{\geq N}) \to M \in ℕ$