Theorem atancl

Description: Closure for the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015)

	Ref	Expression
Assertion	atancl	$$⊢A\in \mathrm{dom}arctan\to arctan\left(A\right)\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		atanf	$$⊢arctan:ℂ\setminus \left\{-\mathrm{i},\mathrm{i}\right\}⟶ℂ$$
2	1	ffvelcdmi	$$⊢A\in \left(ℂ\setminus \left\{-\mathrm{i},\mathrm{i}\right\}\right)\to arctan\left(A\right)\in ℂ$$
3	1	fdmi	$$⊢\mathrm{dom}arctan=ℂ\setminus \left\{-\mathrm{i},\mathrm{i}\right\}$$
4	2 3	eleq2s	$$⊢A\in \mathrm{dom}arctan\to arctan\left(A\right)\in ℂ$$