Metamath Proof Explorer

Theorem znegcl

Description: Closure law for negative integers. (Contributed by NM, 9-May-2004)

Ref Expression
Assertion znegcl ⊢ N ∈ ℤ → − N ∈ ℤ

Proof

Step Hyp Ref Expression
1 elz ⊢ N ∈ ℤ ↔ N ∈ ℝ ∧ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ
2 negeq ⊢ N = 0 → − N = − 0
3 neg0 ⊢ − 0 = 0
4 2 3 eqtrdi ⊢ N = 0 → − N = 0
5 0z ⊢ 0 ∈ ℤ
6 4 5 eqeltrdi ⊢ N = 0 → − N ∈ ℤ
7 nnnegz ⊢ N ∈ ℕ → − N ∈ ℤ
8 nnz ⊢ − N ∈ ℕ → − N ∈ ℤ
9 6 7 8 3jaoi ⊢ N = 0 ∨ N ∈ ℕ ∨ − N ∈ ℕ → − N ∈ ℤ
10 1 9 simplbiim ⊢ N ∈ ℤ → − N ∈ ℤ