Theorem lmdvglim

Description: If a monotonic real number sequence F diverges, it converges in the extended real numbers and its limit is plus infinity. (Contributed by Thierry Arnoux, 3-Aug-2017)

	Ref	Expression
Hypotheses	lmdvglim.j	$$⊢J=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)$$
	lmdvglim.1	$$⊢\phi \to F:\mathbb{N}⟶\left[0,\mathrm{+\infty }\right)$$
	lmdvglim.2	$$⊢\left(\phi \wedge k\in \mathbb{N}\right)\to F\left(k\right)\le F\left(k+1\right)$$
	lmdvglim.3	$$⊢\phi \to \neg F\in \mathrm{dom}⇝$$
Assertion	lmdvglim	$$⊢\phi \to F\underset{t}{⇝}\left(J\right)\mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		lmdvglim.j	$$⊢J=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)$$
2		lmdvglim.1	$$⊢\phi \to F:\mathbb{N}⟶\left[0,\mathrm{+\infty }\right)$$
3		lmdvglim.2	$$⊢\left(\phi \wedge k\in \mathbb{N}\right)\to F\left(k\right)\le F\left(k+1\right)$$
4		lmdvglim.3	$$⊢\phi \to \neg F\in \mathrm{dom}⇝$$
5	2 3 4	lmdvg	$$⊢\phi \to \forall x\in ℝ\exists j\in \mathbb{N}\forall k\in {\mathbb{Z}}_{\ge j}x<F\left(k\right)$$
6		icossicc	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq \left[0,\mathrm{+\infty }\right]$$
7		fss	$$⊢\left(F:\mathbb{N}⟶\left[0,\mathrm{+\infty }\right)\wedge \left[0,\mathrm{+\infty }\right)\subseteq \left[0,\mathrm{+\infty }\right]\right)\to F:\mathbb{N}⟶\left[0,\mathrm{+\infty }\right]$$
8	2 6 7	sylancl	$$⊢\phi \to F:\mathbb{N}⟶\left[0,\mathrm{+\infty }\right]$$
9		eqidd	$$⊢\left(\phi \wedge k\in \mathbb{N}\right)\to F\left(k\right)=F\left(k\right)$$
10	1 8 9	lmxrge0	$$⊢\phi \to \left(F\underset{t}{⇝}\left(J\right)\mathrm{+\infty }\leftrightarrow \forall x\in ℝ\exists j\in \mathbb{N}\forall k\in {\mathbb{Z}}_{\ge j}x<F\left(k\right)\right)$$
11	5 10	mpbird	$$⊢\phi \to F\underset{t}{⇝}\left(J\right)\mathrm{+\infty }$$