Metamath Proof Explorer

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

Proof

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