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

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→ ℂ )