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 ⊢ D = ℂ ∖ −∞ 0
atansopn.s ⊢ S = y ∈ ℂ | 1 + y 2 ∈ D
Assertion atansssdm ⊢ S ⊆ dom ⁡ arctan

Proof

Step Hyp Ref Expression
1 atansopn.d ⊢ D = ℂ ∖ −∞ 0
2 atansopn.s ⊢ S = y ∈ ℂ | 1 + y 2 ∈ D
3 rabss ⊢ y ∈ ℂ | 1 + y 2 ∈ D ⊆ dom ⁡ arctan ↔ ∀ y ∈ ℂ 1 + y 2 ∈ D → y ∈ dom ⁡ arctan
4 simpl ⊢ y ∈ ℂ ∧ 1 + y 2 ∈ D → y ∈ ℂ
5 1 logdmn0 ⊢ 1 + y 2 ∈ D → 1 + y 2 ≠ 0
6 5 adantl ⊢ y ∈ ℂ ∧ 1 + y 2 ∈ D → 1 + y 2 ≠ 0
7 atandm4 ⊢ y ∈ dom ⁡ arctan ↔ y ∈ ℂ ∧ 1 + y 2 ≠ 0
8 4 6 7 sylanbrc ⊢ y ∈ ℂ ∧ 1 + y 2 ∈ D → y ∈ dom ⁡ arctan
9 8 ex ⊢ y ∈ ℂ → 1 + y 2 ∈ D → y ∈ dom ⁡ arctan
10 3 9 mprgbir ⊢ y ∈ ℂ | 1 + y 2 ∈ D ⊆ dom ⁡ arctan
11 2 10 eqsstri ⊢ S ⊆ dom ⁡ arctan