Metamath Proof Explorer

Theorem xlimclim

Description: Given a sequence of reals, it converges to a real number A w.r.t. the standard topology on the reals, if and only if it converges to A w.r.t. to the standard topology on the extended reals (see climreeq ). (Contributed by Glauco Siliprandi, 5-Feb-2022)

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

Proof

Step Hyp Ref Expression
1 xlimclim.m 
 |-  ( ph -> M e. ZZ )
2 xlimclim.z 
 |-  Z = ( ZZ>= ` M )
3 xlimclim.f 
 |-  ( ph -> F : Z --> RR )
4 xlimclim.a 
 |-  ( ph -> A e. RR )
5 df-xlim 
 |-  ~~>* = ( ~~>t ` ( ordTop ` <_ ) )
6 5 breqi 
 |-  ( F ~~>* A <-> F ( ~~>t ` ( ordTop ` <_ ) ) A )
7 6 a1i 
 |-  ( ph -> ( F ~~>* A <-> F ( ~~>t ` ( ordTop ` <_ ) ) A ) )
8 xrtgioo2 
 |-  ( topGen ` ran (,) ) = ( ( ordTop ` <_ ) |`t RR )
9 reex 
 |-  RR e. _V
10 9 a1i 
 |-  ( ph -> RR e. _V )
11 letop 
 |-  ( ordTop ` <_ ) e. Top
12 11 a1i 
 |-  ( ph -> ( ordTop ` <_ ) e. Top )
13 8 2 10 12 4 1 3 lmss 
 |-  ( ph -> ( F ( ~~>t ` ( ordTop ` <_ ) ) A <-> F ( ~~>t ` ( topGen ` ran (,) ) ) A ) )
14 eqid 
 |-  ( ~~>t ` ( topGen ` ran (,) ) ) = ( ~~>t ` ( topGen ` ran (,) ) )
15 14 2 1 3 climreeq 
 |-  ( ph -> ( F ( ~~>t ` ( topGen ` ran (,) ) ) A <-> F ~~> A ) )
16 7 13 15 3bitrd 
 |-  ( ph -> ( F ~~>* A <-> F ~~> A ) )