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

Metamath Proof Explorer

Theorem nnnegz

Description: The negative of a positive integer is an integer. (Contributed by NM, 12-Jan-2002)

Ref Expression
Assertion nnnegz ⊢ N ∈ ℕ → − N ∈ ℤ

Proof

Step Hyp Ref Expression
1 nnre ⊢ N ∈ ℕ → N ∈ ℝ
2 1 renegcld ⊢ N ∈ ℕ → − N ∈ ℝ
3 nncn ⊢ N ∈ ℕ → N ∈ ℂ
4 negneg ⊢ N ∈ ℂ → − -N = N
5 4 eleq1d ⊢ N ∈ ℂ → − -N ∈ ℕ ↔ N ∈ ℕ
6 5 biimprd ⊢ N ∈ ℂ → N ∈ ℕ → − -N ∈ ℕ
7 3 6 mpcom ⊢ N ∈ ℕ → − -N ∈ ℕ
8 7 3mix3d ⊢ N ∈ ℕ → − N = 0 ∨ − N ∈ ℕ ∨ − -N ∈ ℕ
9 elz ⊢ − N ∈ ℤ ↔ − N ∈ ℝ ∧ − N = 0 ∨ − N ∈ ℕ ∨ − -N ∈ ℕ
10 2 8 9 sylanbrc ⊢ N ∈ ℕ → − N ∈ ℤ