Step |
Hyp |
Ref |
Expression |
1 |
|
atansopn.d |
⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) ) |
2 |
|
atansopn.s |
⊢ 𝑆 = { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 } |
3 |
|
rabss |
⊢ ( { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 } ⊆ dom arctan ↔ ∀ 𝑦 ∈ ℂ ( ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 → 𝑦 ∈ dom arctan ) ) |
4 |
|
simpl |
⊢ ( ( 𝑦 ∈ ℂ ∧ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 ) → 𝑦 ∈ ℂ ) |
5 |
1
|
logdmn0 |
⊢ ( ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 → ( 1 + ( 𝑦 ↑ 2 ) ) ≠ 0 ) |
6 |
5
|
adantl |
⊢ ( ( 𝑦 ∈ ℂ ∧ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 ) → ( 1 + ( 𝑦 ↑ 2 ) ) ≠ 0 ) |
7 |
|
atandm4 |
⊢ ( 𝑦 ∈ dom arctan ↔ ( 𝑦 ∈ ℂ ∧ ( 1 + ( 𝑦 ↑ 2 ) ) ≠ 0 ) ) |
8 |
4 6 7
|
sylanbrc |
⊢ ( ( 𝑦 ∈ ℂ ∧ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 ) → 𝑦 ∈ dom arctan ) |
9 |
8
|
ex |
⊢ ( 𝑦 ∈ ℂ → ( ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 → 𝑦 ∈ dom arctan ) ) |
10 |
3 9
|
mprgbir |
⊢ { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 } ⊆ dom arctan |
11 |
2 10
|
eqsstri |
⊢ 𝑆 ⊆ dom arctan |