Metamath Proof Explorer


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