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 \in ℂ \| 1 + y^{2} \in D\}$
	Assertion	atansssdm	$⊢ S \subseteq dom arctan$

Proof

Step	Hyp	Ref	Expression
1		atansopn.d	$⊢ D = ℂ ∖ (−∞, 0]$
2		atansopn.s	$⊢ S = \{y \in ℂ \| 1 + y^{2} \in D\}$
3		rabss	$⊢ \{y \in ℂ \| 1 + y^{2} \in D\} \subseteq dom arctan \leftrightarrow \forall y \in ℂ (1 + y^{2} \in D \to y \in dom arctan)$
4		simpl	$⊢ (y \in ℂ \land 1 + y^{2} \in D) \to y \in ℂ$
5	1	logdmn0	$⊢ 1 + y^{2} \in D \to 1 + y^{2} \neq 0$
6	5	adantl	$⊢ (y \in ℂ \land 1 + y^{2} \in D) \to 1 + y^{2} \neq 0$
7		atandm4	$⊢ y \in dom arctan \leftrightarrow (y \in ℂ \land 1 + y^{2} \neq 0)$
8	4 6 7	sylanbrc	$⊢ (y \in ℂ \land 1 + y^{2} \in D) \to y \in dom arctan$
9	8	ex	$⊢ y \in ℂ \to (1 + y^{2} \in D \to y \in dom arctan)$
10	3 9	mprgbir	$⊢ \{y \in ℂ \| 1 + y^{2} \in D\} \subseteq dom arctan$
11	2 10	eqsstri	$⊢ S \subseteq dom arctan$