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 )