ressatans

Description: The real number line is a subset of the domain of continuity 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	ressatans	$⊢ ℝ \subseteq S$

Proof

Step	Hyp	Ref	Expression
1		atansopn.d	$⊢ D = ℂ ∖ (−∞, 0]$
2		atansopn.s	$⊢ S = \{y \in ℂ \| 1 + y^{2} \in D\}$
3		ax-resscn	$⊢ ℝ \subseteq ℂ$
4		1re	$⊢ 1 \in ℝ$
5		resqcl	$⊢ y \in ℝ \to y^{2} \in ℝ$
6		readdcl	$⊢ (1 \in ℝ \land y^{2} \in ℝ) \to 1 + y^{2} \in ℝ$
7	4 5 6	sylancr	$⊢ y \in ℝ \to 1 + y^{2} \in ℝ$
8	7	recnd	$⊢ y \in ℝ \to 1 + y^{2} \in ℂ$
9	4	a1i	$⊢ y \in ℝ \to 1 \in ℝ$
10		0lt1	$⊢ 0 < 1$
11	10	a1i	$⊢ y \in ℝ \to 0 < 1$
12		sqge0	$⊢ y \in ℝ \to 0 \leq y^{2}$
13	9 5 11 12	addgtge0d	$⊢ y \in ℝ \to 0 < 1 + y^{2}$
14		0re	$⊢ 0 \in ℝ$
15		ltnle	$⊢ (0 \in ℝ \land 1 + y^{2} \in ℝ) \to (0 < 1 + y^{2} \leftrightarrow \neg 1 + y^{2} \leq 0)$
16	14 7 15	sylancr	$⊢ y \in ℝ \to (0 < 1 + y^{2} \leftrightarrow \neg 1 + y^{2} \leq 0)$
17	13 16	mpbid	$⊢ y \in ℝ \to \neg 1 + y^{2} \leq 0$
18		mnfxr	$⊢ −∞ \in ℝ^{*}$
19		elioc2	$⊢ (−∞ \in ℝ^{*} \land 0 \in ℝ) \to (1 + y^{2} \in (−∞, 0] \leftrightarrow (1 + y^{2} \in ℝ \land −∞ < 1 + y^{2} \land 1 + y^{2} \leq 0))$
20	18 14 19	mp2an	$⊢ 1 + y^{2} \in (−∞, 0] \leftrightarrow (1 + y^{2} \in ℝ \land −∞ < 1 + y^{2} \land 1 + y^{2} \leq 0)$
21	20	simp3bi	$⊢ 1 + y^{2} \in (−∞, 0] \to 1 + y^{2} \leq 0$
22	17 21	nsyl	$⊢ y \in ℝ \to \neg 1 + y^{2} \in (−∞, 0]$
23	8 22	eldifd	$⊢ y \in ℝ \to 1 + y^{2} \in (ℂ ∖ (−∞, 0])$
24	23 1	eleqtrrdi	$⊢ y \in ℝ \to 1 + y^{2} \in D$
25	24	rgen	$⊢ \forall y \in ℝ 1 + y^{2} \in D$
26		ssrab	$⊢ ℝ \subseteq \{y \in ℂ \| 1 + y^{2} \in D\} \leftrightarrow (ℝ \subseteq ℂ \land \forall y \in ℝ 1 + y^{2} \in D)$
27	3 25 26	mpbir2an	$⊢ ℝ \subseteq \{y \in ℂ \| 1 + y^{2} \in D\}$
28	27 2	sseqtrri	$⊢ ℝ \subseteq S$

Metamath Proof Explorer

Theorem ressatans

Proof