Theorem 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	⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
	atansopn.s	⊢ 𝑆 = { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 }
Assertion	ressatans	⊢ ℝ ⊆ 𝑆

Proof

Step	Hyp	Ref	Expression
1		atansopn.d	⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2		atansopn.s	⊢ 𝑆 = { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 }
3		ax-resscn	⊢ ℝ ⊆ ℂ
4		1re	⊢ 1 ∈ ℝ
5		resqcl	⊢ ( 𝑦 ∈ ℝ → ( 𝑦 ↑ 2 ) ∈ ℝ )
6		readdcl	⊢ ( ( 1 ∈ ℝ ∧ ( 𝑦 ↑ 2 ) ∈ ℝ ) → ( 1 + ( 𝑦 ↑ 2 ) ) ∈ ℝ )
7	4 5 6	sylancr	⊢ ( 𝑦 ∈ ℝ → ( 1 + ( 𝑦 ↑ 2 ) ) ∈ ℝ )
8	7	recnd	⊢ ( 𝑦 ∈ ℝ → ( 1 + ( 𝑦 ↑ 2 ) ) ∈ ℂ )
9	4	a1i	⊢ ( 𝑦 ∈ ℝ → 1 ∈ ℝ )
10		0lt1	⊢ 0 < 1
11	10	a1i	⊢ ( 𝑦 ∈ ℝ → 0 < 1 )
12		sqge0	⊢ ( 𝑦 ∈ ℝ → 0 ≤ ( 𝑦 ↑ 2 ) )
13	9 5 11 12	addgtge0d	⊢ ( 𝑦 ∈ ℝ → 0 < ( 1 + ( 𝑦 ↑ 2 ) ) )
14		0re	⊢ 0 ∈ ℝ
15		ltnle	⊢ ( ( 0 ∈ ℝ ∧ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ ℝ ) → ( 0 < ( 1 + ( 𝑦 ↑ 2 ) ) ↔ ¬ ( 1 + ( 𝑦 ↑ 2 ) ) ≤ 0 ) )
16	14 7 15	sylancr	⊢ ( 𝑦 ∈ ℝ → ( 0 < ( 1 + ( 𝑦 ↑ 2 ) ) ↔ ¬ ( 1 + ( 𝑦 ↑ 2 ) ) ≤ 0 ) )
17	13 16	mpbid	⊢ ( 𝑦 ∈ ℝ → ¬ ( 1 + ( 𝑦 ↑ 2 ) ) ≤ 0 )
18		mnfxr	⊢ -∞ ∈ ℝ*
19		elioc2	⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ ) → ( ( 1 + ( 𝑦 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ↔ ( ( 1 + ( 𝑦 ↑ 2 ) ) ∈ ℝ ∧ -∞ < ( 1 + ( 𝑦 ↑ 2 ) ) ∧ ( 1 + ( 𝑦 ↑ 2 ) ) ≤ 0 ) ) )
20	18 14 19	mp2an	⊢ ( ( 1 + ( 𝑦 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ↔ ( ( 1 + ( 𝑦 ↑ 2 ) ) ∈ ℝ ∧ -∞ < ( 1 + ( 𝑦 ↑ 2 ) ) ∧ ( 1 + ( 𝑦 ↑ 2 ) ) ≤ 0 ) )
21	20	simp3bi	⊢ ( ( 1 + ( 𝑦 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) → ( 1 + ( 𝑦 ↑ 2 ) ) ≤ 0 )
22	17 21	nsyl	⊢ ( 𝑦 ∈ ℝ → ¬ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) )
23	8 22	eldifd	⊢ ( 𝑦 ∈ ℝ → ( 1 + ( 𝑦 ↑ 2 ) ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
24	23 1	eleqtrrdi	⊢ ( 𝑦 ∈ ℝ → ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 )
25	24	rgen	⊢ ∀ 𝑦 ∈ ℝ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷
26		ssrab	⊢ ( ℝ ⊆ { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 } ↔ ( ℝ ⊆ ℂ ∧ ∀ 𝑦 ∈ ℝ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 ) )
27	3 25 26	mpbir2an	⊢ ℝ ⊆ { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 }
28	27 2	sseqtrri	⊢ ℝ ⊆ 𝑆