Theorem xlimres

Description: A function converges iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	xlimres.1	|- ( ph -> F e. ( RR* ^pm CC ) )
	xlimres.2	|- ( ph -> M e. ZZ )
Assertion	xlimres	|- ( ph -> ( F ~~>* A <-> ( F |` ( ZZ>= ` M ) ) ~~>* A ) )

Proof

Step	Hyp	Ref	Expression
1		xlimres.1	|- ( ph -> F e. ( RR* ^pm CC ) )
2		xlimres.2	|- ( ph -> M e. ZZ )
3		letopon	|- ( ordTop ` <_ ) e. ( TopOn ` RR* )
4	3	a1i	|- ( ph -> ( ordTop ` <_ ) e. ( TopOn ` RR* ) )
5	4 1 2	lmres	|- ( ph -> ( F ( ~~>t ` ( ordTop ` <_ ) ) A <-> ( F |` ( ZZ>= ` M ) ) ( ~~>t ` ( ordTop ` <_ ) ) A ) )
6		df-xlim	|- ~~>* = ( ~~>t ` ( ordTop ` <_ ) )
7	6	breqi	|- ( F ~~>* A <-> F ( ~~>t ` ( ordTop ` <_ ) ) A )
8	6	breqi	|- ( ( F |` ( ZZ>= ` M ) ) ~~>* A <-> ( F |` ( ZZ>= ` M ) ) ( ~~>t ` ( ordTop ` <_ ) ) A )
9	5 7 8	3bitr4g	|- ( ph -> ( F ~~>* A <-> ( F |` ( ZZ>= ` M ) ) ~~>* A ) )