Metamath Proof Explorer


Theorem atans

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 ) ) ∈ 𝐷 ) )

Proof

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 ) ) ∈ 𝐷 ) )