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

Metamath Proof Explorer

Theorem climreclf

Description: The limit of a convergent real sequence is real. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses climreclf.k 
|- F/ k ph
climreclf.f 
|- F/_ k F
climreclf.z 
|- Z = ( ZZ>= ` M )
climreclf.m 
|- ( ph -> M e. ZZ )
climreclf.a 
|- ( ph -> F ~~> A )
climreclf.r 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
Assertion climreclf 
|- ( ph -> A e. RR )

Proof

Step Hyp Ref Expression
1 climreclf.k 
 |-  F/ k ph
2 climreclf.f 
 |-  F/_ k F
3 climreclf.z 
 |-  Z = ( ZZ>= ` M )
4 climreclf.m 
 |-  ( ph -> M e. ZZ )
5 climreclf.a 
 |-  ( ph -> F ~~> A )
6 climreclf.r 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
7 nfv 
 |-  F/ k j e. Z
8 1 7 nfan 
 |-  F/ k ( ph /\ j e. Z )
9 nfcv 
 |-  F/_ k j
10 2 9 nffv 
 |-  F/_ k ( F ` j )
11 nfcv 
 |-  F/_ k RR
12 10 11 nfel 
 |-  F/ k ( F ` j ) e. RR
13 8 12 nfim 
 |-  F/ k ( ( ph /\ j e. Z ) -> ( F ` j ) e. RR )
14 eleq1w 
 |-  ( k = j -> ( k e. Z <-> j e. Z ) )
15 14 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. Z ) <-> ( ph /\ j e. Z ) ) )
16 fveq2 
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
17 16 eleq1d 
 |-  ( k = j -> ( ( F ` k ) e. RR <-> ( F ` j ) e. RR ) )
18 15 17 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR ) <-> ( ( ph /\ j e. Z ) -> ( F ` j ) e. RR ) ) )
19 13 18 6 chvarfv 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) e. RR )
20 3 4 5 19 climrecl 
 |-  ( ph -> A e. RR )