This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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