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

Metamath Proof Explorer

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