Theorem atans

Description: The "domain of continuity" of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015)

	Ref	Expression
Hypotheses	atansopn.d	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
	atansopn.s	$$⊢S=\left\{y\in ℂ|1+y^2\in D\right\}$$
Assertion	atans	$$⊢A\in S\leftrightarrow \left(A\in ℂ\wedge 1+A^2\in D\right)$$

Proof

Step	Hyp	Ref	Expression
1		atansopn.d	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
2		atansopn.s	$$⊢S=\left\{y\in ℂ|1+y^2\in D\right\}$$
3		oveq1	$$⊢y=A\to y^2=A^2$$
4	3	oveq2d	$$⊢y=A\to 1+y^2=1+A^2$$
5	4	eleq1d	$$⊢y=A\to \left(1+y^2\in D\leftrightarrow 1+A^2\in D\right)$$
6	5 2	elrab2	$$⊢A\in S\leftrightarrow \left(A\in ℂ\wedge 1+A^2\in D\right)$$