xlimconst2

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

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

Proof

Step	Hyp	Ref	Expression
1		xlimconst2.p	\|- F/ k ph
2		xlimconst2.k	\|- F/_ k F
3		xlimconst2.z	\|- Z = ( ZZ>= ` M )
4		xlimconst2.f	\|- ( ph -> F : Z --> RR* )
5		xlimconst2.n	\|- ( ph -> N e. Z )
6		xlimconst2.a	\|- ( ph -> A e. RR* )
7		xlimconst2.e	\|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( F ` k ) = A )
8		nfcv	\|- F/_ k ( ZZ>= ` N )
9	2 8	nfres	\|- F/_ k ( F \|` ( ZZ>= ` N ) )
10	3 5	eluzelz2d	\|- ( ph -> N e. ZZ )
11		eqid	\|- ( ZZ>= ` N ) = ( ZZ>= ` N )
12	4	ffnd	\|- ( ph -> F Fn Z )
13	3 5	uzssd2	\|- ( ph -> ( ZZ>= ` N ) C_ Z )
14	12 13	fnssresd	\|- ( ph -> ( F \|` ( ZZ>= ` N ) ) Fn ( ZZ>= ` N ) )
15		fvres	\|- ( k e. ( ZZ>= ` N ) -> ( ( F \|` ( ZZ>= ` N ) ) ` k ) = ( F ` k ) )
16	15	adantl	\|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( F \|` ( ZZ>= ` N ) ) ` k ) = ( F ` k ) )
17	16 7	eqtrd	\|- ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( F \|` ( ZZ>= ` N ) ) ` k ) = A )
18	1 9 10 11 14 6 17	xlimconst	\|- ( ph -> ( F \|` ( ZZ>= ` N ) ) ~~>* A )
19	3 4	fuzxrpmcn	\|- ( ph -> F e. ( RR* ^pm CC ) )
20	19 10	xlimres	\|- ( ph -> ( F ~~>* A <-> ( F \|` ( ZZ>= ` N ) ) ~~>* A ) )
21	18 20	mpbird	\|- ( ph -> F ~~>* A )

Metamath Proof Explorer

Theorem xlimconst2

Proof