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 = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
	lmdvglim.1	|- ( ph -> F : NN --> ( 0 [,) +oo ) )
	lmdvglim.2	|- ( ( ph /\ k e. NN ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )
	lmdvglim.3	|- ( ph -> -. F e. dom ~~> )
Assertion	lmdvglim	|- ( ph -> F ( ~~>t ` J ) +oo )

Proof

Step	Hyp	Ref	Expression
1		lmdvglim.j	|- J = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
2		lmdvglim.1	|- ( ph -> F : NN --> ( 0 [,) +oo ) )
3		lmdvglim.2	|- ( ( ph /\ k e. NN ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )
4		lmdvglim.3	|- ( ph -> -. F e. dom ~~> )
5	2 3 4	lmdvg	|- ( ph -> A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < ( F ` k ) )
6		icossicc	|- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
7		fss	|- ( ( F : NN --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ ( 0 [,] +oo ) ) -> F : NN --> ( 0 [,] +oo ) )
8	2 6 7	sylancl	|- ( ph -> F : NN --> ( 0 [,] +oo ) )
9		eqidd	|- ( ( ph /\ k e. NN ) -> ( F ` k ) = ( F ` k ) )
10	1 8 9	lmxrge0	|- ( ph -> ( F ( ~~>t ` J ) +oo <-> A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < ( F ` k ) ) )
11	5 10	mpbird	|- ( ph -> F ( ~~>t ` J ) +oo )