Theorem climi0

Description: Convergence of a sequence of complex numbers to zero. (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$$
	climi0.5	$$⊢\phi \to F⇝0$$
Assertion	climi0	$$⊢\phi \to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|B\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		climi0.5	$$⊢\phi \to F⇝0$$
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-0\right|<C\right)$$
7		subid1	$$⊢B\in ℂ\to B-0=B$$
8	7	fveq2d	$$⊢B\in ℂ\to \left|B-0\right|=\left|B\right|$$
9	8	breq1d	$$⊢B\in ℂ\to \left(\left|B-0\right|<C\leftrightarrow \left|B\right|<C\right)$$
10	9	biimpa	$$⊢\left(B\in ℂ\wedge \left|B-0\right|<C\right)\to \left|B\right|<C$$
11	10	ralimi	$$⊢\forall k\in {\mathbb{Z}}_{\ge j}\left(B\in ℂ\wedge \left|B-0\right|<C\right)\to \forall k\in {\mathbb{Z}}_{\ge j}\left|B\right|<C$$
12	11	reximi	$$⊢\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(B\in ℂ\wedge \left|B-0\right|<C\right)\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|B\right|<C$$
13	6 12	syl	$$⊢\phi \to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|B\right|<C$$