Metamath Proof Explorer

Theorem xlimconst

Description: A constant sequence converges to its value, w.r.t. the standard topology on the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022)

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

Proof

Step Hyp Ref Expression
1 xlimconst.p 
 |-  F/ k ph
2 xlimconst.k 
 |-  F/_ k F
3 xlimconst.m 
 |-  ( ph -> M e. ZZ )
4 xlimconst.z 
 |-  Z = ( ZZ>= ` M )
5 xlimconst.f 
 |-  ( ph -> F Fn Z )
6 xlimconst.a 
 |-  ( ph -> A e. RR* )
7 xlimconst.e 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
8 1 2 5 6 7 fconst7 
 |-  ( ph -> F = ( Z X. { A } ) )
9 letopon 
 |-  ( ordTop ` <_ ) e. ( TopOn ` RR* )
10 4 lmconst 
 |-  ( ( ( ordTop ` <_ ) e. ( TopOn ` RR* ) /\ A e. RR* /\ M e. ZZ ) -> ( Z X. { A } ) ( ~~>t ` ( ordTop ` <_ ) ) A )
11 9 6 3 10 mp3an2i 
 |-  ( ph -> ( Z X. { A } ) ( ~~>t ` ( ordTop ` <_ ) ) A )
12 8 11 eqbrtrd 
 |-  ( ph -> F ( ~~>t ` ( ordTop ` <_ ) ) A )
13 df-xlim 
 |-  ~~>* = ( ~~>t ` ( ordTop ` <_ ) )
14 13 breqi 
 |-  ( F ~~>* A <-> F ( ~~>t ` ( ordTop ` <_ ) ) A )
15 12 14 sylibr 
 |-  ( ph -> F ~~>* A )