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 ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℤ ↔ - 𝐴 ∈ ℤ ) )

Proof

Step Hyp Ref Expression
1 znegcl ( 𝐴 ∈ ℤ → - 𝐴 ∈ ℤ )
2 znegcl ( - 𝐴 ∈ ℤ → - - 𝐴 ∈ ℤ )
3 negneg ( 𝐴 ∈ ℂ → - - 𝐴 = 𝐴 )
4 3 eleq1d ( 𝐴 ∈ ℂ → ( - - 𝐴 ∈ ℤ ↔ 𝐴 ∈ ℤ ) )
5 2 4 syl5ib ( 𝐴 ∈ ℂ → ( - 𝐴 ∈ ℤ → 𝐴 ∈ ℤ ) )
6 1 5 impbid2 ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℤ ↔ - 𝐴 ∈ ℤ ) )