Theorem climreclmpt

Description: The limit of B convergent real sequence is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	climreclmpt.k	|- F/ k ph
	climreclmpt.m	|- ( ph -> M e. ZZ )
	climreclmpt.z	|- Z = ( ZZ>= ` M )
	climreclmpt.a	|- ( ( ph /\ k e. Z ) -> A e. RR )
	climreclmpt.b	|- ( ph -> ( k e. Z |-> A ) ~~> B )
Assertion	climreclmpt	|- ( ph -> B e. RR )

Proof

Step	Hyp	Ref	Expression
1		climreclmpt.k	|- F/ k ph
2		climreclmpt.m	|- ( ph -> M e. ZZ )
3		climreclmpt.z	|- Z = ( ZZ>= ` M )
4		climreclmpt.a	|- ( ( ph /\ k e. Z ) -> A e. RR )
5		climreclmpt.b	|- ( ph -> ( k e. Z |-> A ) ~~> B )
6		nfmpt1	|- F/_ k ( k e. Z |-> A )
7		eqidd	|- ( ph -> ( k e. Z |-> A ) = ( k e. Z |-> A ) )
8	7 4	fvmpt2d	|- ( ( ph /\ k e. Z ) -> ( ( k e. Z |-> A ) ` k ) = A )
9	8 4	eqeltrd	|- ( ( ph /\ k e. Z ) -> ( ( k e. Z |-> A ) ` k ) e. RR )
10	1 6 3 2 5 9	climreclf	|- ( ph -> B e. RR )