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={\mathbb{Z}}_{\ge M}$$
	climeq.2	$$⊢\phi \to F\in V$$
	climeq.3	$$⊢\phi \to G\in W$$
	climeq.5	$$⊢\phi \to M\in \mathbb{Z}$$
	climeq.6	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=G\left(k\right)$$
Assertion	climeq	$$⊢\phi \to \left(F⇝A\leftrightarrow G⇝A\right)$$

Proof

Step	Hyp	Ref	Expression
1		climeq.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		climeq.2	$$⊢\phi \to F\in V$$
3		climeq.3	$$⊢\phi \to G\in W$$
4		climeq.5	$$⊢\phi \to M\in \mathbb{Z}$$
5		climeq.6	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=G\left(k\right)$$
6	1 4 2 5	clim2	$$⊢\phi \to \left(F⇝A\leftrightarrow \left(A\in ℂ\wedge \forall x\in {ℝ}^{+}\exists y\in Z\forall k\in {\mathbb{Z}}_{\ge y}\left(G\left(k\right)\in ℂ\wedge \left|G\left(k\right)-A\right|<x\right)\right)\right)$$
7		eqidd	$$⊢\left(\phi \wedge k\in Z\right)\to G\left(k\right)=G\left(k\right)$$
8	1 4 3 7	clim2	$$⊢\phi \to \left(G⇝A\leftrightarrow \left(A\in ℂ\wedge \forall x\in {ℝ}^{+}\exists y\in Z\forall k\in {\mathbb{Z}}_{\ge y}\left(G\left(k\right)\in ℂ\wedge \left|G\left(k\right)-A\right|<x\right)\right)\right)$$
9	6 8	bitr4d	$$⊢\phi \to \left(F⇝A\leftrightarrow G⇝A\right)$$