# Metamath Proof Explorer

## Theorem climrescn

Description: A sequence converging w.r.t. the standard topology on the complex numbers, eventually becomes a sequence of complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses climrescn.m ${⊢}{\phi }\to {M}\in ℤ$
climrescn.z ${⊢}{Z}={ℤ}_{\ge {M}}$
climrescn.f ${⊢}{\phi }\to {F}Fn{Z}$
climrescn.c ${⊢}{\phi }\to {F}\in \mathrm{dom}⇝$
Assertion climrescn ${⊢}{\phi }\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶ℂ$

### Proof

Step Hyp Ref Expression
1 climrescn.m ${⊢}{\phi }\to {M}\in ℤ$
2 climrescn.z ${⊢}{Z}={ℤ}_{\ge {M}}$
3 climrescn.f ${⊢}{\phi }\to {F}Fn{Z}$
4 climrescn.c ${⊢}{\phi }\to {F}\in \mathrm{dom}⇝$
5 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {i}\in {Z}\right)$
6 nfra1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)$
7 5 6 nfan ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {i}\in {Z}\right)\wedge \forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)\right)$
8 2 uztrn2 ${⊢}\left({i}\in {Z}\wedge {k}\in {ℤ}_{\ge {i}}\right)\to {k}\in {Z}$
9 8 adantll ${⊢}\left(\left({\phi }\wedge {i}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {i}}\right)\to {k}\in {Z}$
10 3 fndmd ${⊢}{\phi }\to \mathrm{dom}{F}={Z}$
11 10 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {i}}\right)\to \mathrm{dom}{F}={Z}$
12 9 11 eleqtrrd ${⊢}\left(\left({\phi }\wedge {i}\in {Z}\right)\wedge {k}\in {ℤ}_{\ge {i}}\right)\to {k}\in \mathrm{dom}{F}$
13 12 adantlr ${⊢}\left(\left(\left({\phi }\wedge {i}\in {Z}\right)\wedge \forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)\right)\wedge {k}\in {ℤ}_{\ge {i}}\right)\to {k}\in \mathrm{dom}{F}$
14 rspa ${⊢}\left(\forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)\wedge {k}\in {ℤ}_{\ge {i}}\right)\to \left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)$
15 14 adantll ${⊢}\left(\left({i}\in {Z}\wedge \forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)\right)\wedge {k}\in {ℤ}_{\ge {i}}\right)\to \left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)$
16 15 simpld ${⊢}\left(\left({i}\in {Z}\wedge \forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)\right)\wedge {k}\in {ℤ}_{\ge {i}}\right)\to {F}\left({k}\right)\in ℂ$
17 16 adantlll ${⊢}\left(\left(\left({\phi }\wedge {i}\in {Z}\right)\wedge \forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)\right)\wedge {k}\in {ℤ}_{\ge {i}}\right)\to {F}\left({k}\right)\in ℂ$
18 13 17 jca ${⊢}\left(\left(\left({\phi }\wedge {i}\in {Z}\right)\wedge \forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)\right)\wedge {k}\in {ℤ}_{\ge {i}}\right)\to \left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in ℂ\right)$
19 7 18 ralrimia ${⊢}\left(\left({\phi }\wedge {i}\in {Z}\right)\wedge \forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)\right)\to \forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in ℂ\right)$
20 fnfun ${⊢}{F}Fn{Z}\to \mathrm{Fun}{F}$
21 ffvresb ${⊢}\mathrm{Fun}{F}\to \left(\left({{F}↾}_{{ℤ}_{\ge {i}}}\right):{ℤ}_{\ge {i}}⟶ℂ↔\forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in ℂ\right)\right)$
22 3 20 21 3syl ${⊢}{\phi }\to \left(\left({{F}↾}_{{ℤ}_{\ge {i}}}\right):{ℤ}_{\ge {i}}⟶ℂ↔\forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in ℂ\right)\right)$
23 22 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in {Z}\right)\wedge \forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)\right)\to \left(\left({{F}↾}_{{ℤ}_{\ge {i}}}\right):{ℤ}_{\ge {i}}⟶ℂ↔\forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in ℂ\right)\right)$
24 19 23 mpbird ${⊢}\left(\left({\phi }\wedge {i}\in {Z}\right)\wedge \forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)\right)\to \left({{F}↾}_{{ℤ}_{\ge {i}}}\right):{ℤ}_{\ge {i}}⟶ℂ$
25 breq2 ${⊢}{x}=1\to \left(\left|{F}\left({k}\right)-⇝\left({F}\right)\right|<{x}↔\left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)$
26 25 anbi2d ${⊢}{x}=1\to \left(\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<{x}\right)↔\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)\right)$
27 26 rexralbidv ${⊢}{x}=1\to \left(\exists {i}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<{x}\right)↔\exists {i}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)\right)$
28 climdm ${⊢}{F}\in \mathrm{dom}⇝↔{F}⇝⇝\left({F}\right)$
29 4 28 sylib ${⊢}{\phi }\to {F}⇝⇝\left({F}\right)$
30 eqidd ${⊢}\left({\phi }\wedge {k}\in ℤ\right)\to {F}\left({k}\right)={F}\left({k}\right)$
31 4 30 clim ${⊢}{\phi }\to \left({F}⇝⇝\left({F}\right)↔\left(⇝\left({F}\right)\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {i}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<{x}\right)\right)\right)$
32 29 31 mpbid ${⊢}{\phi }\to \left(⇝\left({F}\right)\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {i}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<{x}\right)\right)$
33 32 simprd ${⊢}{\phi }\to \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {i}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<{x}\right)$
34 1rp ${⊢}1\in {ℝ}^{+}$
35 34 a1i ${⊢}{\phi }\to 1\in {ℝ}^{+}$
36 27 33 35 rspcdva ${⊢}{\phi }\to \exists {i}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)$
37 2 rexuz3 ${⊢}{M}\in ℤ\to \left(\exists {i}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)↔\exists {i}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)\right)$
38 1 37 syl ${⊢}{\phi }\to \left(\exists {i}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)↔\exists {i}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)\right)$
39 36 38 mpbird ${⊢}{\phi }\to \exists {i}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-⇝\left({F}\right)\right|<1\right)$
40 24 39 reximddv3 ${⊢}{\phi }\to \exists {i}\in {Z}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right):{ℤ}_{\ge {i}}⟶ℂ$
41 fveq2 ${⊢}{j}={i}\to {ℤ}_{\ge {j}}={ℤ}_{\ge {i}}$
42 41 reseq2d ${⊢}{j}={i}\to {{F}↾}_{{ℤ}_{\ge {j}}}={{F}↾}_{{ℤ}_{\ge {i}}}$
43 42 41 feq12d ${⊢}{j}={i}\to \left(\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶ℂ↔\left({{F}↾}_{{ℤ}_{\ge {i}}}\right):{ℤ}_{\ge {i}}⟶ℂ\right)$
44 43 cbvrexvw ${⊢}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶ℂ↔\exists {i}\in {Z}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {i}}}\right):{ℤ}_{\ge {i}}⟶ℂ$
45 40 44 sylibr ${⊢}{\phi }\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶ℂ$