Theorem climeldmeqf

Description: Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		climeldmeqf.p	|- F/ k ph
2		climeldmeqf.n	|- F/_ k F
3		climeldmeqf.o	|- F/_ k G
4		climeldmeqf.z	|- Z = ( ZZ>= ` M )
5		climeldmeqf.f	|- ( ph -> F e. V )
6		climeldmeqf.g	|- ( ph -> G e. W )
7		climeldmeqf.m	|- ( ph -> M e. ZZ )
8		climeldmeqf.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	4 5 6 7 22	climeldmeq	|- ( ph -> ( F e. dom ~~> <-> G e. dom ~~> ) )