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=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)$$
	lmlimxrge0.f	$$⊢\phi \to F:\mathbb{N}⟶X$$
	lmlimxrge0.p	$$⊢\phi \to P\in X$$
	lmlimxrge0.x	$$⊢X\subseteq \left[0,\mathrm{+\infty }\right)$$
Assertion	lmlimxrge0	$$⊢\phi \to \left(F\underset{t}{⇝}\left(J\right)P\leftrightarrow F⇝P\right)$$

Proof

Step	Hyp	Ref	Expression
1		lmlimxrge0.j	$$⊢J=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)$$
2		lmlimxrge0.f	$$⊢\phi \to F:\mathbb{N}⟶X$$
3		lmlimxrge0.p	$$⊢\phi \to P\in X$$
4		lmlimxrge0.x	$$⊢X\subseteq \left[0,\mathrm{+\infty }\right)$$
5		xrge0topn	$$⊢\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]$$
6	1 5	eqtri	$$⊢J=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]$$
7		letopon	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)$$
8		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
9		resttopon	$$⊢\left(\mathrm{ordTop}\left(\le \right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)\wedge \left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}\right)\to \mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]\in \mathrm{TopOn}\left(\left[0,\mathrm{+\infty }\right]\right)$$
10	7 8 9	mp2an	$$⊢\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]\in \mathrm{TopOn}\left(\left[0,\mathrm{+\infty }\right]\right)$$
11	6 10	eqeltri	$$⊢J\in \mathrm{TopOn}\left(\left[0,\mathrm{+\infty }\right]\right)$$
12		fvex	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{V}$$
13		icossicc	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq \left[0,\mathrm{+\infty }\right]$$
14	4 13	sstri	$$⊢X\subseteq \left[0,\mathrm{+\infty }\right]$$
15		ovex	$$⊢\left[0,\mathrm{+\infty }\right]\in \mathrm{V}$$
16		restabs	$$⊢\left(\mathrm{ordTop}\left(\le \right)\in \mathrm{V}\wedge X\subseteq \left[0,\mathrm{+\infty }\right]\wedge \left[0,\mathrm{+\infty }\right]\in \mathrm{V}\right)\to \left(\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]\right){\upharpoonright }_{𝑡}X=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}X$$
17	12 14 15 16	mp3an	$$⊢\left(\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]\right){\upharpoonright }_{𝑡}X=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}X$$
18	6	oveq1i	$$⊢J{\upharpoonright }_{𝑡}X=\left(\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}\left[0,\mathrm{+\infty }\right]\right){\upharpoonright }_{𝑡}X$$
19		rge0ssre	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq ℝ$$
20	4 19	sstri	$$⊢X\subseteq ℝ$$
21		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
22		eqid	$$⊢\mathrm{ordTop}\left(\le \right)=\mathrm{ordTop}\left(\le \right)$$
23	21 22	xrrest2	$$⊢X\subseteq ℝ\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}X$$
24	20 23	ax-mp	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}X$$
25	17 18 24	3eqtr4i	$$⊢J{\upharpoonright }_{𝑡}X=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X$$
26		ax-resscn	$$⊢ℝ\subseteq ℂ$$
27	20 26	sstri	$$⊢X\subseteq ℂ$$
28	11 2 3 25 27	lmlim	$$⊢\phi \to \left(F\underset{t}{⇝}\left(J\right)P\leftrightarrow F⇝P\right)$$