Theorem climeqf

Description: Two functions that are eventually equal to one another have the same limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	climeqf.p	|- F/ k ph
	climeqf.k	|- F/_ k F
	climeqf.n	|- F/_ k G
	climeqf.m	|- ( ph -> M e. ZZ )
	climeqf.z	|- Z = ( ZZ>= ` M )
	climeqf.f	|- ( ph -> F e. V )
	climeqf.g	|- ( ph -> G e. W )
	climeqf.e	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` k ) )
Assertion	climeqf	|- ( ph -> ( F ~~> A <-> G ~~> A ) )

Proof

Step	Hyp	Ref	Expression
1		climeqf.p	|- F/ k ph
2		climeqf.k	|- F/_ k F
3		climeqf.n	|- F/_ k G
4		climeqf.m	|- ( ph -> M e. ZZ )
5		climeqf.z	|- Z = ( ZZ>= ` M )
6		climeqf.f	|- ( ph -> F e. V )
7		climeqf.g	|- ( ph -> G e. W )
8		climeqf.e	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` k ) )
9		nfv	|- F/ k j e. Z
10	1 9	nfan	|- F/ k ( ph /\ j e. Z )
11		nfcv	|- F/_ k j
12	2 11	nffv	|- F/_ k ( F ` j )
13	3 11	nffv	|- F/_ k ( G ` j )
14	12 13	nfeq	|- F/ k ( F ` j ) = ( G ` j )
15	10 14	nfim	|- F/ k ( ( ph /\ j e. Z ) -> ( F ` j ) = ( G ` j ) )
16		eleq1w	|- ( k = j -> ( k e. Z <-> j e. Z ) )
17	16	anbi2d	|- ( k = j -> ( ( ph /\ k e. Z ) <-> ( ph /\ j e. Z ) ) )
18		fveq2	|- ( k = j -> ( F ` k ) = ( F ` j ) )
19		fveq2	|- ( k = j -> ( G ` k ) = ( G ` j ) )
20	18 19	eqeq12d	|- ( k = j -> ( ( F ` k ) = ( G ` k ) <-> ( F ` j ) = ( G ` j ) ) )
21	17 20	imbi12d	|- ( k = j -> ( ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` k ) ) <-> ( ( ph /\ j e. Z ) -> ( F ` j ) = ( G ` j ) ) ) )
22	15 21 8	chvarfv	|- ( ( ph /\ j e. Z ) -> ( F ` j ) = ( G ` j ) )
23	5 6 7 4 22	climeq	|- ( ph -> ( F ~~> A <-> G ~~> A ) )