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

Metamath Proof Explorer

Theorem nnz

Description: A positive integer is an integer. (Contributed by NM, 9-May-2004) Reduce dependencies on axioms. (Revised by Steven Nguyen, 29-Nov-2022)

Ref Expression
Assertion nnz ⊢ N ∈ ℕ → N ∈ ℤ

Proof

Step Hyp Ref Expression
1 nnre ⊢ N ∈ ℕ → N ∈ ℝ
2 3mix2 ⊢ N ∈ ℕ → N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ
3 elz ⊢ N ∈ ℤ ↔ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ
4 1 2 3 sylanbrc ⊢ N ∈ ℕ → N ∈ ℤ