# Metamath Proof Explorer

## 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}={ℤ}_{\ge {M}}$
climi.2 ${⊢}{\phi }\to {M}\in ℤ$
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}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{B}-{A}\right|<{C}$

### Proof

Step Hyp Ref Expression
1 climi.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 climi.2 ${⊢}{\phi }\to {M}\in ℤ$
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}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\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 {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({B}\in ℂ\wedge \left|{B}-{A}\right|<{C}\right)\to \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{B}-{A}\right|<{C}$
9 8 reximi ${⊢}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({B}\in ℂ\wedge \left|{B}-{A}\right|<{C}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{B}-{A}\right|<{C}$
10 6 9 syl ${⊢}{\phi }\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|{B}-{A}\right|<{C}$