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

Metamath Proof Explorer

Theorem nnuz

Description: Positive integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005)

Ref Expression
Assertion nnuz ⊢ ℕ = ℤ ≥ 1

Proof

Step Hyp Ref Expression
1 nnzrab ⊢ ℕ = k ∈ ℤ | 1 ≤ k
2 1z ⊢ 1 ∈ ℤ
3 uzval ⊢ 1 ∈ ℤ → ℤ ≥ 1 = k ∈ ℤ | 1 ≤ k
4 2 3 ax-mp ⊢ ℤ ≥ 1 = k ∈ ℤ | 1 ≤ k
5 1 4 eqtr4i ⊢ ℕ = ℤ ≥ 1