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

Metamath Proof Explorer

Theorem elnnuz

Description: A positive integer expressed as a member of an upper set of integers. (Contributed by NM, 6-Jun-2006)

Ref Expression
Assertion elnnuz ⊢ N ∈ ℕ ↔ N ∈ ℤ ≥ 1

Proof

Step Hyp Ref Expression
1 nnuz ⊢ ℕ = ℤ ≥ 1
2 1 eleq2i ⊢ N ∈ ℕ ↔ N ∈ ℤ ≥ 1