# Metamath Proof Explorer

## Theorem climleltrp

Description: The limit of complex number sequence F is eventually approximated. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses climleltrp.k ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
climleltrp.f ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{F}$
climleltrp.z ${⊢}{Z}={ℤ}_{\ge {M}}$
climleltrp.n ${⊢}{\phi }\to {N}\in {Z}$
climleltrp.r ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\to {F}\left({k}\right)\in ℝ$
climleltrp.a ${⊢}{\phi }\to {F}⇝{A}$
climleltrp.c ${⊢}{\phi }\to {C}\in ℝ$
climleltrp.l ${⊢}{\phi }\to {A}\le {C}$
climleltrp.x ${⊢}{\phi }\to {X}\in {ℝ}^{+}$
Assertion climleltrp ${⊢}{\phi }\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℝ\wedge {F}\left({k}\right)<{C}+{X}\right)$

### Proof

Step Hyp Ref Expression
1 climleltrp.k ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
2 climleltrp.f ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{F}$
3 climleltrp.z ${⊢}{Z}={ℤ}_{\ge {M}}$
4 climleltrp.n ${⊢}{\phi }\to {N}\in {Z}$
5 climleltrp.r ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\to {F}\left({k}\right)\in ℝ$
6 climleltrp.a ${⊢}{\phi }\to {F}⇝{A}$
7 climleltrp.c ${⊢}{\phi }\to {C}\in ℝ$
8 climleltrp.l ${⊢}{\phi }\to {A}\le {C}$
9 climleltrp.x ${⊢}{\phi }\to {X}\in {ℝ}^{+}$
10 4 3 eleqtrdi ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
11 uzss ${⊢}{N}\in {ℤ}_{\ge {M}}\to {ℤ}_{\ge {N}}\subseteq {ℤ}_{\ge {M}}$
12 10 11 syl ${⊢}{\phi }\to {ℤ}_{\ge {N}}\subseteq {ℤ}_{\ge {M}}$
13 12 3 sseqtrrdi ${⊢}{\phi }\to {ℤ}_{\ge {N}}\subseteq {Z}$
14 uzssz ${⊢}{ℤ}_{\ge {M}}\subseteq ℤ$
15 14 10 sseldi ${⊢}{\phi }\to {N}\in ℤ$
16 eqid ${⊢}{ℤ}_{\ge {N}}={ℤ}_{\ge {N}}$
17 eqidd ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\to {F}\left({k}\right)={F}\left({k}\right)$
18 1 2 15 16 6 17 9 clim2d ${⊢}{\phi }\to \exists {j}\in {ℤ}_{\ge {N}}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)$
19 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{j}\in {ℤ}_{\ge {N}}$
20 1 19 nfan ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {j}\in {ℤ}_{\ge {N}}\right)$
21 simplll ${⊢}\left(\left(\left({\phi }\wedge {j}\in {ℤ}_{\ge {N}}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {\phi }$
22 uzss ${⊢}{j}\in {ℤ}_{\ge {N}}\to {ℤ}_{\ge {j}}\subseteq {ℤ}_{\ge {N}}$
23 22 ad2antlr ${⊢}\left(\left({\phi }\wedge {j}\in {ℤ}_{\ge {N}}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {ℤ}_{\ge {j}}\subseteq {ℤ}_{\ge {N}}$
24 simpr ${⊢}\left(\left({\phi }\wedge {j}\in {ℤ}_{\ge {N}}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {k}\in {ℤ}_{\ge {j}}$
25 23 24 sseldd ${⊢}\left(\left({\phi }\wedge {j}\in {ℤ}_{\ge {N}}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {k}\in {ℤ}_{\ge {N}}$
26 25 adantr ${⊢}\left(\left(\left({\phi }\wedge {j}\in {ℤ}_{\ge {N}}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {k}\in {ℤ}_{\ge {N}}$
27 simpr ${⊢}\left(\left(\left({\phi }\wedge {j}\in {ℤ}_{\ge {N}}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to \left|{F}\left({k}\right)-{A}\right|<{X}$
28 17 5 eqeltrd ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\to {F}\left({k}\right)\in ℝ$
29 28 adantr ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {F}\left({k}\right)\in ℝ$
30 climcl ${⊢}{F}⇝{A}\to {A}\in ℂ$
31 6 30 syl ${⊢}{\phi }\to {A}\in ℂ$
32 31 adantr ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\to {A}\in ℂ$
33 28 recnd ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\to {F}\left({k}\right)\in ℂ$
34 32 33 pncan3d ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\to {A}+{F}\left({k}\right)-{A}={F}\left({k}\right)$
35 34 eqcomd ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\to {F}\left({k}\right)={A}+{F}\left({k}\right)-{A}$
36 35 adantr ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {F}\left({k}\right)={A}+{F}\left({k}\right)-{A}$
37 36 29 eqeltrrd ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {A}+{F}\left({k}\right)-{A}\in ℝ$
38 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {C}\in ℝ$
39 1 2 16 15 6 5 climreclf ${⊢}{\phi }\to {A}\in ℝ$
40 39 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {A}\in ℝ$
41 29 40 resubcld ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {F}\left({k}\right)-{A}\in ℝ$
42 38 41 readdcld ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {C}+{F}\left({k}\right)-{A}\in ℝ$
43 9 rpred ${⊢}{\phi }\to {X}\in ℝ$
44 43 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {X}\in ℝ$
45 38 44 readdcld ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {C}+{X}\in ℝ$
46 8 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {A}\le {C}$
47 40 38 41 46 leadd1dd ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {A}+{F}\left({k}\right)-{A}\le {C}+{F}\left({k}\right)-{A}$
48 33 adantr ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {F}\left({k}\right)\in ℂ$
49 32 adantr ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {A}\in ℂ$
50 48 49 subcld ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {F}\left({k}\right)-{A}\in ℂ$
51 50 abscld ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to \left|{F}\left({k}\right)-{A}\right|\in ℝ$
52 41 leabsd ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {F}\left({k}\right)-{A}\le \left|{F}\left({k}\right)-{A}\right|$
53 simpr ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to \left|{F}\left({k}\right)-{A}\right|<{X}$
54 41 51 44 52 53 lelttrd ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {F}\left({k}\right)-{A}<{X}$
55 41 44 38 54 ltadd2dd ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {C}+{F}\left({k}\right)-{A}<{C}+{X}$
56 37 42 45 47 55 lelttrd ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {A}+{F}\left({k}\right)-{A}<{C}+{X}$
57 36 56 eqbrtrd ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to {F}\left({k}\right)<{C}+{X}$
58 29 57 jca ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {N}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to \left({F}\left({k}\right)\in ℝ\wedge {F}\left({k}\right)<{C}+{X}\right)$
59 21 26 27 58 syl21anc ${⊢}\left(\left(\left({\phi }\wedge {j}\in {ℤ}_{\ge {N}}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to \left({F}\left({k}\right)\in ℝ\wedge {F}\left({k}\right)<{C}+{X}\right)$
60 59 adantrl ${⊢}\left(\left(\left({\phi }\wedge {j}\in {ℤ}_{\ge {N}}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge \left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\right)\to \left({F}\left({k}\right)\in ℝ\wedge {F}\left({k}\right)<{C}+{X}\right)$
61 60 ex ${⊢}\left(\left({\phi }\wedge {j}\in {ℤ}_{\ge {N}}\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to \left(\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to \left({F}\left({k}\right)\in ℝ\wedge {F}\left({k}\right)<{C}+{X}\right)\right)$
62 20 61 ralimdaa ${⊢}\left({\phi }\wedge {j}\in {ℤ}_{\ge {N}}\right)\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℝ\wedge {F}\left({k}\right)<{C}+{X}\right)\right)$
63 62 reximdva ${⊢}{\phi }\to \left(\exists {j}\in {ℤ}_{\ge {N}}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℂ\wedge \left|{F}\left({k}\right)-{A}\right|<{X}\right)\to \exists {j}\in {ℤ}_{\ge {N}}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℝ\wedge {F}\left({k}\right)<{C}+{X}\right)\right)$
64 18 63 mpd ${⊢}{\phi }\to \exists {j}\in {ℤ}_{\ge {N}}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℝ\wedge {F}\left({k}\right)<{C}+{X}\right)$
65 ssrexv ${⊢}{ℤ}_{\ge {N}}\subseteq {Z}\to \left(\exists {j}\in {ℤ}_{\ge {N}}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℝ\wedge {F}\left({k}\right)<{C}+{X}\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℝ\wedge {F}\left({k}\right)<{C}+{X}\right)\right)$
66 13 64 65 sylc ${⊢}{\phi }\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({k}\right)\in ℝ\wedge {F}\left({k}\right)<{C}+{X}\right)$