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=ℂ∖−∞0
atansopn.s ⊢S=y∈ℂ|1+y2∈D
Assertion atansopn ⊢S∈TopOpen⁡ℂfld

Proof

Step Hyp Ref Expression
1 atansopn.d ⊢D=ℂ∖−∞0
2 atansopn.s ⊢S=y∈ℂ|1+y2∈D
3 eqid ⊢y∈ℂ⟼1+y2=y∈ℂ⟼1+y2
4 3 mptpreima ⊢y∈ℂ⟼1+y2-1D=y∈ℂ|1+y2∈D
5 2 4 eqtr4i ⊢S=y∈ℂ⟼1+y2-1D
6 eqid ⊢TopOpen⁡ℂfld=TopOpen⁡ℂfld
7 6 cnfldtopon ⊢TopOpen⁡ℂfld∈TopOn⁡ℂ
8 7 a1i ⊢⊤→TopOpen⁡ℂfld∈TopOn⁡ℂ
9 1cnd ⊢⊤→1∈ℂ
10 8 8 9 cnmptc ⊢⊤→y∈ℂ⟼1∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
11 2nn0 ⊢2∈ℕ0
12 6 expcn ⊢2∈ℕ0→y∈ℂ⟼y2∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
13 11 12 mp1i ⊢⊤→y∈ℂ⟼y2∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
14 6 addcn ⊢+∈TopOpen⁡ℂfld×tTopOpen⁡ℂfldCnTopOpen⁡ℂfld
15 14 a1i ⊢⊤→+∈TopOpen⁡ℂfld×tTopOpen⁡ℂfldCnTopOpen⁡ℂfld
16 8 10 13 15 cnmpt12f ⊢⊤→y∈ℂ⟼1+y2∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
17 16 mptru ⊢y∈ℂ⟼1+y2∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld
18 1 logdmopn ⊢D∈TopOpen⁡ℂfld
19 cnima ⊢y∈ℂ⟼1+y2∈TopOpen⁡ℂfldCnTopOpen⁡ℂfld∧D∈TopOpen⁡ℂfld→y∈ℂ⟼1+y2-1D∈TopOpen⁡ℂfld
20 17 18 19 mp2an ⊢y∈ℂ⟼1+y2-1D∈TopOpen⁡ℂfld
21 5 20 eqeltri ⊢S∈TopOpen⁡ℂfld