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 + y 2 ∈ D
Assertion atansopn ⊢ S ∈ TopOpen ⁡ ℂ fld

Proof

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