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	imbitrid	⊢ ( 𝐴 ∈ ℂ → ( - 𝐴 ∈ ℤ → 𝐴 ∈ ℤ ) )
6	1 5	impbid2	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℤ ↔ - 𝐴 ∈ ℤ ) )