Theorem climxlim

Description: A converging sequence in the reals is a converging sequence in the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	climxlim.m	|- ( ph -> M e. ZZ )
	climxlim.z	|- Z = ( ZZ>= ` M )
	climxlim.f	|- ( ph -> F : Z --> RR )
	climxlim.c	|- ( ph -> F ~~> A )
Assertion	climxlim	|- ( ph -> F ~~>* A )

Proof

Step	Hyp	Ref	Expression
1		climxlim.m	|- ( ph -> M e. ZZ )
2		climxlim.z	|- Z = ( ZZ>= ` M )
3		climxlim.f	|- ( ph -> F : Z --> RR )
4		climxlim.c	|- ( ph -> F ~~> A )
5	3	ffvelrnda	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
6	2 1 4 5	climrecl	|- ( ph -> A e. RR )
7	1 2 3 6	xlimclim	|- ( ph -> ( F ~~>* A <-> F ~~> A ) )
8	4 7	mpbird	|- ( ph -> F ~~>* A )