Metamath Proof Explorer

Theorem lmlimxrge0

Description: Relate a limit in the nonnegative extended reals to a complex limit, provided the considered function is a real function. (Contributed by Thierry Arnoux, 11-Jul-2017)

Ref Expression
Hypotheses lmlimxrge0.j ⊢ J = TopOpen ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞
lmlimxrge0.f ⊢ φ → F : ℕ ⟶ X
lmlimxrge0.p ⊢ φ → P ∈ X
lmlimxrge0.x ⊢ X ⊆ 0 +∞
Assertion lmlimxrge0 ⊢ φ → F ⇝t ⁡ J P ↔ F ⇝ P

Proof

Step Hyp Ref Expression
1 lmlimxrge0.j ⊢ J = TopOpen ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞
2 lmlimxrge0.f ⊢ φ → F : ℕ ⟶ X
3 lmlimxrge0.p ⊢ φ → P ∈ X
4 lmlimxrge0.x ⊢ X ⊆ 0 +∞
5 xrge0topn ⊢ TopOpen ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞ = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
6 1 5 eqtri ⊢ J = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
7 letopon ⊢ ordTop ⁡ ≤ ∈ TopOn ⁡ ℝ *
8 iccssxr ⊢ 0 +∞ ⊆ ℝ *
9 resttopon ⊢ ordTop ⁡ ≤ ∈ TopOn ⁡ ℝ * ∧ 0 +∞ ⊆ ℝ * → ordTop ⁡ ≤ ↾ 𝑡 0 +∞ ∈ TopOn ⁡ 0 +∞
10 7 8 9 mp2an ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ ∈ TopOn ⁡ 0 +∞
11 6 10 eqeltri ⊢ J ∈ TopOn ⁡ 0 +∞
12 fvex ⊢ ordTop ⁡ ≤ ∈ V
13 icossicc ⊢ 0 +∞ ⊆ 0 +∞
14 4 13 sstri ⊢ X ⊆ 0 +∞
15 ovex ⊢ 0 +∞ ∈ V
16 restabs ⊢ ordTop ⁡ ≤ ∈ V ∧ X ⊆ 0 +∞ ∧ 0 +∞ ∈ V → ordTop ⁡ ≤ ↾ 𝑡 0 +∞ ↾ 𝑡 X = ordTop ⁡ ≤ ↾ 𝑡 X
17 12 14 15 16 mp3an ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ ↾ 𝑡 X = ordTop ⁡ ≤ ↾ 𝑡 X
18 6 oveq1i ⊢ J ↾ 𝑡 X = ordTop ⁡ ≤ ↾ 𝑡 0 +∞ ↾ 𝑡 X
19 rge0ssre ⊢ 0 +∞ ⊆ ℝ
20 4 19 sstri ⊢ X ⊆ ℝ
21 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
22 eqid ⊢ ordTop ⁡ ≤ = ordTop ⁡ ≤
23 21 22 xrrest2 ⊢ X ⊆ ℝ → TopOpen ⁡ ℂ fld ↾ 𝑡 X = ordTop ⁡ ≤ ↾ 𝑡 X
24 20 23 ax-mp ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 X = ordTop ⁡ ≤ ↾ 𝑡 X
25 17 18 24 3eqtr4i ⊢ J ↾ 𝑡 X = TopOpen ⁡ ℂ fld ↾ 𝑡 X
26 ax-resscn ⊢ ℝ ⊆ ℂ
27 20 26 sstri ⊢ X ⊆ ℂ
28 11 2 3 25 27 lmlim ⊢ φ → F ⇝t ⁡ J P ↔ F ⇝ P