Theorem climeq

Description: Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 5-Nov-2013) (Revised by Mario Carneiro, 31-Jan-2014)

	Ref	Expression
Hypotheses	climeq.1	|- Z = ( ZZ>= ` M )
	climeq.2	|- ( ph -> F e. V )
	climeq.3	|- ( ph -> G e. W )
	climeq.5	|- ( ph -> M e. ZZ )
	climeq.6	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` k ) )
Assertion	climeq	|- ( ph -> ( F ~~> A <-> G ~~> A ) )

Proof

Step	Hyp	Ref	Expression
1		climeq.1	|- Z = ( ZZ>= ` M )
2		climeq.2	|- ( ph -> F e. V )
3		climeq.3	|- ( ph -> G e. W )
4		climeq.5	|- ( ph -> M e. ZZ )
5		climeq.6	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` k ) )
6	1 4 2 5	clim2	|- ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. y e. Z A. k e. ( ZZ>= ` y ) ( ( G ` k ) e. CC /\ ( abs ` ( ( G ` k ) - A ) ) < x ) ) ) )
7		eqidd	|- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( G ` k ) )
8	1 4 3 7	clim2	|- ( ph -> ( G ~~> A <-> ( A e. CC /\ A. x e. RR+ E. y e. Z A. k e. ( ZZ>= ` y ) ( ( G ` k ) e. CC /\ ( abs ` ( ( G ` k ) - A ) ) < x ) ) ) )
9	6 8	bitr4d	|- ( ph -> ( F ~~> A <-> G ~~> A ) )