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

Metamath Proof Explorer

Theorem climrecl

Description: The limit of a convergent real sequence is real. Corollary 12-2.5 of Gleason p. 172. (Contributed by NM, 10-Sep-2005) (Proof shortened by Mario Carneiro, 10-May-2016)

Ref Expression
Hypotheses climshft2.1 
|- Z = ( ZZ>= ` M )
climshft2.2 
|- ( ph -> M e. ZZ )
climrecl.3 
|- ( ph -> F ~~> A )
climrecl.4 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
Assertion climrecl 
|- ( ph -> A e. RR )

Proof

Step Hyp Ref Expression
1 climshft2.1 
 |-  Z = ( ZZ>= ` M )
2 climshft2.2 
 |-  ( ph -> M e. ZZ )
3 climrecl.3 
 |-  ( ph -> F ~~> A )
4 climrecl.4 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
5 1 uzsup 
 |-  ( M e. ZZ -> sup ( Z , RR* , < ) = +oo )
6 2 5 syl 
 |-  ( ph -> sup ( Z , RR* , < ) = +oo )
7 climrel 
 |-  Rel ~~>
8 7 brrelex1i 
 |-  ( F ~~> A -> F e. _V )
9 3 8 syl 
 |-  ( ph -> F e. _V )
10 eqid 
 |-  ( k e. Z |-> ( F ` k ) ) = ( k e. Z |-> ( F ` k ) )
11 1 10 climmpt 
 |-  ( ( M e. ZZ /\ F e. _V ) -> ( F ~~> A <-> ( k e. Z |-> ( F ` k ) ) ~~> A ) )
12 2 9 11 syl2anc 
 |-  ( ph -> ( F ~~> A <-> ( k e. Z |-> ( F ` k ) ) ~~> A ) )
13 3 12 mpbid 
 |-  ( ph -> ( k e. Z |-> ( F ` k ) ) ~~> A )
14 4 recnd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
15 14 fmpttd 
 |-  ( ph -> ( k e. Z |-> ( F ` k ) ) : Z --> CC )
16 1 2 15 rlimclim 
 |-  ( ph -> ( ( k e. Z |-> ( F ` k ) ) ~~>r A <-> ( k e. Z |-> ( F ` k ) ) ~~> A ) )
17 13 16 mpbird 
 |-  ( ph -> ( k e. Z |-> ( F ` k ) ) ~~>r A )
18 6 17 4 rlimrecl 
 |-  ( ph -> A e. RR )