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

Metamath Proof Explorer

Theorem znegcl

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

Ref Expression
Assertion znegcl ( 𝑁 ∈ ℤ → - 𝑁 ∈ ℤ )

Proof

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