This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 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 ⊢ ℝ ⊆ 𝑆