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	⊢ 𝐽 = ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
	lmlimxrge0.f	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑋 )
	lmlimxrge0.p	⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
	lmlimxrge0.x	⊢ 𝑋 ⊆ ( 0 [,) +∞ )
Assertion	lmlimxrge0	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ 𝐹 ⇝ 𝑃 ) )

Proof

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