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

Metamath Proof Explorer

Theorem climconst

Description: An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses climconst.1 
|- Z = ( ZZ>= ` M )
climconst.2 
|- ( ph -> M e. ZZ )
climconst.3 
|- ( ph -> F e. V )
climconst.4 
|- ( ph -> A e. CC )
climconst.5 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
Assertion climconst 
|- ( ph -> F ~~> A )

Proof

Step Hyp Ref Expression
1 climconst.1 
 |-  Z = ( ZZ>= ` M )
2 climconst.2 
 |-  ( ph -> M e. ZZ )
3 climconst.3 
 |-  ( ph -> F e. V )
4 climconst.4 
 |-  ( ph -> A e. CC )
5 climconst.5 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
6 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
7 2 6 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
8 7 1 eleqtrrdi 
 |-  ( ph -> M e. Z )
9 4 subidd 
 |-  ( ph -> ( A - A ) = 0 )
10 9 fveq2d 
 |-  ( ph -> ( abs ` ( A - A ) ) = ( abs ` 0 ) )
11 abs0 
 |-  ( abs ` 0 ) = 0
12 10 11 eqtrdi 
 |-  ( ph -> ( abs ` ( A - A ) ) = 0 )
13 12 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` ( A - A ) ) = 0 )
14 rpgt0 
 |-  ( x e. RR+ -> 0 < x )
15 14 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> 0 < x )
16 13 15 eqbrtrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` ( A - A ) ) < x )
17 16 ralrimivw 
 |-  ( ( ph /\ x e. RR+ ) -> A. k e. Z ( abs ` ( A - A ) ) < x )
18 fveq2 
 |-  ( j = M -> ( ZZ>= ` j ) = ( ZZ>= ` M ) )
19 18 1 eqtr4di 
 |-  ( j = M -> ( ZZ>= ` j ) = Z )
20 19 raleqdv 
 |-  ( j = M -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( A - A ) ) < x <-> A. k e. Z ( abs ` ( A - A ) ) < x ) )
21 20 rspcev 
 |-  ( ( M e. Z /\ A. k e. Z ( abs ` ( A - A ) ) < x ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( A - A ) ) < x )
22 8 17 21 syl2an2r 
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( A - A ) ) < x )
23 22 ralrimiva 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( A - A ) ) < x )
24 4 adantr 
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
25 1 2 3 5 4 24 clim2c 
 |-  ( ph -> ( F ~~> A <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( A - A ) ) < x ) )
26 23 25 mpbird 
 |-  ( ph -> F ~~> A )