Theorem atancn

Description: The arctangent is a continuous function. (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	atancn	$$⊢\left({arctan\upharpoonright }_S\right):S\underset{cn}{⟶}ℂ$$

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		ssid	$$⊢ℂ\subseteq ℂ$$
4		atanf	$$⊢arctan:ℂ\setminus \left\{-\mathrm{i},\mathrm{i}\right\}⟶ℂ$$
5	1 2	atansssdm	$$⊢S\subseteq \mathrm{dom}arctan$$
6	4	fdmi	$$⊢\mathrm{dom}arctan=ℂ\setminus \left\{-\mathrm{i},\mathrm{i}\right\}$$
7	5 6	sseqtri	$$⊢S\subseteq ℂ\setminus \left\{-\mathrm{i},\mathrm{i}\right\}$$
8		fssres	$$⊢\left(arctan:ℂ\setminus \left\{-\mathrm{i},\mathrm{i}\right\}⟶ℂ\wedge S\subseteq ℂ\setminus \left\{-\mathrm{i},\mathrm{i}\right\}\right)\to \left({arctan\upharpoonright }_S\right):S⟶ℂ$$
9	4 7 8	mp2an	$$⊢\left({arctan\upharpoonright }_S\right):S⟶ℂ$$
10	2	ssrab3	$$⊢S\subseteq ℂ$$
11		ovex	$$⊢\frac{1}{1+x^2}\in \mathrm{V}$$
12	1 2	dvatan	$$⊢ℂ\mathrm{D}\left({arctan\upharpoonright }_S\right)=\left(x\in S⟼\frac{1}{1+x^2}\right)$$
13	11 12	dmmpti	$$⊢\mathrm{dom}{\left({arctan\upharpoonright }_S\right)}_{ℂ}^{\prime }=S$$
14		dvcn	$$⊢\left(\left(ℂ\subseteq ℂ\wedge \left({arctan\upharpoonright }_S\right):S⟶ℂ\wedge S\subseteq ℂ\right)\wedge \mathrm{dom}{\left({arctan\upharpoonright }_S\right)}_{ℂ}^{\prime }=S\right)\to \left({arctan\upharpoonright }_S\right):S\underset{cn}{⟶}ℂ$$
15	13 14	mpan2	$$⊢\left(ℂ\subseteq ℂ\wedge \left({arctan\upharpoonright }_S\right):S⟶ℂ\wedge S\subseteq ℂ\right)\to \left({arctan\upharpoonright }_S\right):S\underset{cn}{⟶}ℂ$$
16	3 9 10 15	mp3an	$$⊢\left({arctan\upharpoonright }_S\right):S\underset{cn}{⟶}ℂ$$