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 ~~> ) )

Metamath Proof Explorer

Theorem climeldmeqf

Proof