This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )