# Metamath Proof Explorer

## Theorem atansopn

Description: The domain of continuity of the arctangent is an open set. (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 atansopn ${⊢}{S}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\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 eqid ${⊢}\left({y}\in ℂ⟼1+{{y}}^{2}\right)=\left({y}\in ℂ⟼1+{{y}}^{2}\right)$
4 3 mptpreima ${⊢}{\left({y}\in ℂ⟼1+{{y}}^{2}\right)}^{-1}\left[{D}\right]=\left\{{y}\in ℂ|1+{{y}}^{2}\in {D}\right\}$
5 2 4 eqtr4i ${⊢}{S}={\left({y}\in ℂ⟼1+{{y}}^{2}\right)}^{-1}\left[{D}\right]$
6 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
7 6 cnfldtopon ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
8 7 a1i ${⊢}\top \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
9 1cnd ${⊢}\top \to 1\in ℂ$
10 8 8 9 cnmptc ${⊢}\top \to \left({y}\in ℂ⟼1\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
11 2nn0 ${⊢}2\in {ℕ}_{0}$
12 6 expcn ${⊢}2\in {ℕ}_{0}\to \left({y}\in ℂ⟼{{y}}^{2}\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
13 11 12 mp1i ${⊢}\top \to \left({y}\in ℂ⟼{{y}}^{2}\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
14 6 addcn ${⊢}+\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
15 14 a1i ${⊢}\top \to +\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
16 8 10 13 15 cnmpt12f ${⊢}\top \to \left({y}\in ℂ⟼1+{{y}}^{2}\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
17 16 mptru ${⊢}\left({y}\in ℂ⟼1+{{y}}^{2}\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
18 1 logdmopn ${⊢}{D}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
19 cnima ${⊢}\left(\left({y}\in ℂ⟼1+{{y}}^{2}\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\wedge {D}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\to {\left({y}\in ℂ⟼1+{{y}}^{2}\right)}^{-1}\left[{D}\right]\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
20 17 18 19 mp2an ${⊢}{\left({y}\in ℂ⟼1+{{y}}^{2}\right)}^{-1}\left[{D}\right]\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
21 5 20 eqeltri ${⊢}{S}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$