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

Metamath Proof Explorer

Theorem znegclb

Description: A complex number is an integer iff its negative is. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion znegclb ⊢ A ∈ ℂ → A ∈ ℤ ↔ − A ∈ ℤ

Proof

Step Hyp Ref Expression
1 znegcl ⊢ A ∈ ℤ → − A ∈ ℤ
2 znegcl ⊢ − A ∈ ℤ → − − A ∈ ℤ
3 negneg ⊢ A ∈ ℂ → − − A = A
4 3 eleq1d ⊢ A ∈ ℂ → − − A ∈ ℤ ↔ A ∈ ℤ
5 2 4 imbitrid ⊢ A ∈ ℂ → − A ∈ ℤ → A ∈ ℤ
6 1 5 impbid2 ⊢ A ∈ ℂ → A ∈ ℤ ↔ − A ∈ ℤ