Theorem atandmneg

Description: The domain of the arctangent function is closed under negatives. (Contributed by Mario Carneiro, 3-Apr-2015)

	Ref	Expression
Assertion	atandmneg	$$⊢A\in \mathrm{dom}arctan\to -A\in \mathrm{dom}arctan$$

Proof

Step	Hyp	Ref	Expression
1		atandm3	$$⊢A\in \mathrm{dom}arctan\leftrightarrow \left(A\in ℂ\wedge A^2\ne -1\right)$$
2	1	simplbi	$$⊢A\in \mathrm{dom}arctan\to A\in ℂ$$
3	2	negcld	$$⊢A\in \mathrm{dom}arctan\to -A\in ℂ$$
4		sqneg	$$⊢A\in ℂ\to {\left(-A\right)}^2=A^2$$
5	2 4	syl	$$⊢A\in \mathrm{dom}arctan\to {\left(-A\right)}^2=A^2$$
6	1	simprbi	$$⊢A\in \mathrm{dom}arctan\to A^2\ne -1$$
7	5 6	eqnetrd	$$⊢A\in \mathrm{dom}arctan\to {\left(-A\right)}^2\ne -1$$
8		atandm3	$$⊢-A\in \mathrm{dom}arctan\leftrightarrow \left(-A\in ℂ\wedge {\left(-A\right)}^2\ne -1\right)$$
9	3 7 8	sylanbrc	$$⊢A\in \mathrm{dom}arctan\to -A\in \mathrm{dom}arctan$$