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\in ℂ\to \left(A\in \mathbb{Z}\leftrightarrow -A\in \mathbb{Z}\right)$$

Proof

Step	Hyp	Ref	Expression
1		znegcl	$$⊢A\in \mathbb{Z}\to -A\in \mathbb{Z}$$
2		znegcl	$$⊢-A\in \mathbb{Z}\to -\left(-A\right)\in \mathbb{Z}$$
3		negneg	$$⊢A\in ℂ\to -\left(-A\right)=A$$
4	3	eleq1d	$$⊢A\in ℂ\to \left(-\left(-A\right)\in \mathbb{Z}\leftrightarrow A\in \mathbb{Z}\right)$$
5	2 4	imbitrid	$$⊢A\in ℂ\to \left(-A\in \mathbb{Z}\to A\in \mathbb{Z}\right)$$
6	1 5	impbid2	$$⊢A\in ℂ\to \left(A\in \mathbb{Z}\leftrightarrow -A\in \mathbb{Z}\right)$$