Theorem atansssdm

Description: The domain of continuity of the arctangent is a subset of the actual domain of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015)

	Ref	Expression
Hypotheses	atansopn.d	⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
	atansopn.s	⊢ 𝑆 = { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 }
Assertion	atansssdm	⊢ 𝑆 ⊆ dom arctan

Proof

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