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