Description: The "domain of continuity" of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | atansopn.d | ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) ) | |
atansopn.s | ⊢ 𝑆 = { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 } | ||
Assertion | atans | ⊢ ( 𝐴 ∈ 𝑆 ↔ ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ 𝐷 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | atansopn.d | ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) ) | |
2 | atansopn.s | ⊢ 𝑆 = { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 } | |
3 | oveq1 | ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ↑ 2 ) = ( 𝐴 ↑ 2 ) ) | |
4 | 3 | oveq2d | ⊢ ( 𝑦 = 𝐴 → ( 1 + ( 𝑦 ↑ 2 ) ) = ( 1 + ( 𝐴 ↑ 2 ) ) ) |
5 | 4 | eleq1d | ⊢ ( 𝑦 = 𝐴 → ( ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 ↔ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ 𝐷 ) ) |
6 | 5 2 | elrab2 | ⊢ ( 𝐴 ∈ 𝑆 ↔ ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ 𝐷 ) ) |