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 )