Metamath Proof Explorer


Theorem atancn

Description: The arctangent is a continuous function. (Contributed by Mario Carneiro, 7-Apr-2015)

Ref Expression
Hypotheses atansopn.d 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
atansopn.s 𝑆 = { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 }
Assertion atancn ( arctan ↾ 𝑆 ) ∈ ( 𝑆cn→ ℂ )

Proof

Step Hyp Ref Expression
1 atansopn.d 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2 atansopn.s 𝑆 = { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 }
3 ssid ℂ ⊆ ℂ
4 atanf arctan : ( ℂ ∖ { - i , i } ) ⟶ ℂ
5 1 2 atansssdm 𝑆 ⊆ dom arctan
6 4 fdmi dom arctan = ( ℂ ∖ { - i , i } )
7 5 6 sseqtri 𝑆 ⊆ ( ℂ ∖ { - i , i } )
8 fssres ( ( arctan : ( ℂ ∖ { - i , i } ) ⟶ ℂ ∧ 𝑆 ⊆ ( ℂ ∖ { - i , i } ) ) → ( arctan ↾ 𝑆 ) : 𝑆 ⟶ ℂ )
9 4 7 8 mp2an ( arctan ↾ 𝑆 ) : 𝑆 ⟶ ℂ
10 2 ssrab3 𝑆 ⊆ ℂ
11 ovex ( 1 / ( 1 + ( 𝑥 ↑ 2 ) ) ) ∈ V
12 1 2 dvatan ( ℂ D ( arctan ↾ 𝑆 ) ) = ( 𝑥𝑆 ↦ ( 1 / ( 1 + ( 𝑥 ↑ 2 ) ) ) )
13 11 12 dmmpti dom ( ℂ D ( arctan ↾ 𝑆 ) ) = 𝑆
14 dvcn ( ( ( ℂ ⊆ ℂ ∧ ( arctan ↾ 𝑆 ) : 𝑆 ⟶ ℂ ∧ 𝑆 ⊆ ℂ ) ∧ dom ( ℂ D ( arctan ↾ 𝑆 ) ) = 𝑆 ) → ( arctan ↾ 𝑆 ) ∈ ( 𝑆cn→ ℂ ) )
15 13 14 mpan2 ( ( ℂ ⊆ ℂ ∧ ( arctan ↾ 𝑆 ) : 𝑆 ⟶ ℂ ∧ 𝑆 ⊆ ℂ ) → ( arctan ↾ 𝑆 ) ∈ ( 𝑆cn→ ℂ ) )
16 3 9 10 15 mp3an ( arctan ↾ 𝑆 ) ∈ ( 𝑆cn→ ℂ )