This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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