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 )