This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
atansopn.s ⊢ 𝑆 = { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 }
Assertion atansopn 𝑆 ∈ ( TopOpen ‘ ℂfld )

Proof

Step Hyp Ref Expression
1 atansopn.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2 atansopn.s ⊢ 𝑆 = { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 }
3 eqid ⊢ ( 𝑦 ∈ ℂ ↦ ( 1 + ( 𝑦 ↑ 2 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 1 + ( 𝑦 ↑ 2 ) ) )
4 3 mptpreima ⊢ ( ◡ ( 𝑦 ∈ ℂ ↦ ( 1 + ( 𝑦 ↑ 2 ) ) ) “ 𝐷 ) = { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 }
5 2 4 eqtr4i ⊢ 𝑆 = ( ◡ ( 𝑦 ∈ ℂ ↦ ( 1 + ( 𝑦 ↑ 2 ) ) ) “ 𝐷 )
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 ⊢ ( ⊤ → ( 𝑦 ∈ ℂ ↦ 1 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
11 2nn0 ⊢ 2 ∈ ℕ0
12 6 expcn ⊢ ( 2 ∈ ℕ0 → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 2 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
13 11 12 mp1i ⊢ ( ⊤ → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 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 ⊢ ( ⊤ → ( 𝑦 ∈ ℂ ↦ ( 1 + ( 𝑦 ↑ 2 ) ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
17 16 mptru ⊢ ( 𝑦 ∈ ℂ ↦ ( 1 + ( 𝑦 ↑ 2 ) ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
18 1 logdmopn ⊢ 𝐷 ∈ ( TopOpen ‘ ℂfld )
19 cnima ⊢ ( ( ( 𝑦 ∈ ℂ ↦ ( 1 + ( 𝑦 ↑ 2 ) ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ∧ 𝐷 ∈ ( TopOpen ‘ ℂfld ) ) → ( ◡ ( 𝑦 ∈ ℂ ↦ ( 1 + ( 𝑦 ↑ 2 ) ) ) “ 𝐷 ) ∈ ( TopOpen ‘ ℂfld ) )
20 17 18 19 mp2an ⊢ ( ◡ ( 𝑦 ∈ ℂ ↦ ( 1 + ( 𝑦 ↑ 2 ) ) ) “ 𝐷 ) ∈ ( TopOpen ‘ ℂfld )
21 5 20 eqeltri ⊢ 𝑆 ∈ ( TopOpen ‘ ℂfld )