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