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