Theorem climi2

Description: Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007) (Revised by Mario Carneiro, 31-Jan-2014)

	Ref	Expression
Hypotheses	climi.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climi.2	$$⊢\phi \to M\in \mathbb{Z}$$
	climi.3	$$⊢\phi \to C\in {ℝ}^{+}$$
	climi.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=B$$
	climi.5	$$⊢\phi \to F⇝A$$
Assertion	climi2	$$⊢\phi \to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|B-A\right|<C$$

Proof

Step	Hyp	Ref	Expression
1		climi.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		climi.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		climi.3	$$⊢\phi \to C\in {ℝ}^{+}$$
4		climi.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=B$$
5		climi.5	$$⊢\phi \to F⇝A$$
6	1 2 3 4 5	climi	$$⊢\phi \to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(B\in ℂ\wedge \left|B-A\right|<C\right)$$
7		simpr	$$⊢\left(B\in ℂ\wedge \left|B-A\right|<C\right)\to \left|B-A\right|<C$$
8	7	ralimi	$$⊢\forall k\in {\mathbb{Z}}_{\ge j}\left(B\in ℂ\wedge \left|B-A\right|<C\right)\to \forall k\in {\mathbb{Z}}_{\ge j}\left|B-A\right|<C$$
9	8	reximi	$$⊢\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(B\in ℂ\wedge \left|B-A\right|<C\right)\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|B-A\right|<C$$
10	6 9	syl	$$⊢\phi \to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|B-A\right|<C$$