# Metamath Proof Explorer

## Theorem climsuse

Description: A subsequence G of a converging sequence F , converges to the same limit. I is the strictly increasing and it is used to index the subsequence. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses climsuse.1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
climsuse.3 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{F}$
climsuse.2 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{G}$
climsuse.4 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{I}$
climsuse.5 ${⊢}{Z}={ℤ}_{\ge {M}}$
climsuse.6 ${⊢}{\phi }\to {M}\in ℤ$
climsuse.7 ${⊢}{\phi }\to {F}\in {X}$
climsuse.8 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in ℂ$
climsuse.9 ${⊢}{\phi }\to {F}⇝{A}$
climsuse.10 ${⊢}{\phi }\to {I}\left({M}\right)\in {Z}$
climsuse.11 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {I}\left({k}+1\right)\in {ℤ}_{\ge \left({I}\left({k}\right)+1\right)}$
climsuse.12 ${⊢}{\phi }\to {G}\in {Y}$
climsuse.13 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)={F}\left({I}\left({k}\right)\right)$
Assertion climsuse ${⊢}{\phi }\to {G}⇝{A}$

### Proof

Step Hyp Ref Expression
1 climsuse.1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
2 climsuse.3 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{F}$
3 climsuse.2 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{G}$
4 climsuse.4 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{I}$
5 climsuse.5 ${⊢}{Z}={ℤ}_{\ge {M}}$
6 climsuse.6 ${⊢}{\phi }\to {M}\in ℤ$
7 climsuse.7 ${⊢}{\phi }\to {F}\in {X}$
8 climsuse.8 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in ℂ$
9 climsuse.9 ${⊢}{\phi }\to {F}⇝{A}$
10 climsuse.10 ${⊢}{\phi }\to {I}\left({M}\right)\in {Z}$
11 climsuse.11 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {I}\left({k}+1\right)\in {ℤ}_{\ge \left({I}\left({k}\right)+1\right)}$
12 climsuse.12 ${⊢}{\phi }\to {G}\in {Y}$
13 climsuse.13 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)={F}\left({I}\left({k}\right)\right)$
14 climcl ${⊢}{F}⇝{A}\to {A}\in ℂ$
15 9 14 syl ${⊢}{\phi }\to {A}\in ℂ$
16 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
17 simpllr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\wedge {M}\le {j}\right)\to {j}\in ℤ$
18 6 ad4antr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\wedge ¬{M}\le {j}\right)\to {M}\in ℤ$
19 17 18 ifclda ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\to if\left({M}\le {j},{j},{M}\right)\in ℤ$
20 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)$
21 nfra1 ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)$
22 20 21 nfan ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)$
23 simp-4l ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {\phi }$
24 simpllr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {j}\in ℤ$
25 23 24 jca ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to \left({\phi }\wedge {j}\in ℤ\right)$
26 simpr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}$
27 simpr ${⊢}\left(\left({\phi }\wedge {j}\in ℤ\right)\wedge {M}\le {j}\right)\to {M}\le {j}$
28 6 anim1i ${⊢}\left({\phi }\wedge {j}\in ℤ\right)\to \left({M}\in ℤ\wedge {j}\in ℤ\right)$
29 28 adantr ${⊢}\left(\left({\phi }\wedge {j}\in ℤ\right)\wedge {M}\le {j}\right)\to \left({M}\in ℤ\wedge {j}\in ℤ\right)$
30 eluz ${⊢}\left({M}\in ℤ\wedge {j}\in ℤ\right)\to \left({j}\in {ℤ}_{\ge {M}}↔{M}\le {j}\right)$
31 29 30 syl ${⊢}\left(\left({\phi }\wedge {j}\in ℤ\right)\wedge {M}\le {j}\right)\to \left({j}\in {ℤ}_{\ge {M}}↔{M}\le {j}\right)$
32 27 31 mpbird ${⊢}\left(\left({\phi }\wedge {j}\in ℤ\right)\wedge {M}\le {j}\right)\to {j}\in {ℤ}_{\ge {M}}$
33 simpll ${⊢}\left(\left({\phi }\wedge {j}\in ℤ\right)\wedge ¬{M}\le {j}\right)\to {\phi }$
34 uzid ${⊢}{M}\in ℤ\to {M}\in {ℤ}_{\ge {M}}$
35 33 6 34 3syl ${⊢}\left(\left({\phi }\wedge {j}\in ℤ\right)\wedge ¬{M}\le {j}\right)\to {M}\in {ℤ}_{\ge {M}}$
36 32 35 ifclda ${⊢}\left({\phi }\wedge {j}\in ℤ\right)\to if\left({M}\le {j},{j},{M}\right)\in {ℤ}_{\ge {M}}$
37 uzss ${⊢}if\left({M}\le {j},{j},{M}\right)\in {ℤ}_{\ge {M}}\to {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\subseteq {ℤ}_{\ge {M}}$
38 36 37 syl ${⊢}\left({\phi }\wedge {j}\in ℤ\right)\to {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\subseteq {ℤ}_{\ge {M}}$
39 38 5 sseqtrrdi ${⊢}\left({\phi }\wedge {j}\in ℤ\right)\to {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\subseteq {Z}$
40 39 sseld ${⊢}\left({\phi }\wedge {j}\in ℤ\right)\to \left({i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\to {i}\in {Z}\right)$
41 25 26 40 sylc ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {i}\in {Z}$
42 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{i}\in {Z}$
43 1 42 nfan ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {i}\in {Z}\right)$
44 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{i}$
45 3 44 nffv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{G}\left({i}\right)$
46 4 44 nffv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{I}\left({i}\right)$
47 2 46 nffv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{F}\left({I}\left({i}\right)\right)$
48 45 47 nfeq ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{G}\left({i}\right)={F}\left({I}\left({i}\right)\right)$
49 43 48 nfim ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {i}\in {Z}\right)\to {G}\left({i}\right)={F}\left({I}\left({i}\right)\right)\right)$
50 eleq1 ${⊢}{k}={i}\to \left({k}\in {Z}↔{i}\in {Z}\right)$
51 50 anbi2d ${⊢}{k}={i}\to \left(\left({\phi }\wedge {k}\in {Z}\right)↔\left({\phi }\wedge {i}\in {Z}\right)\right)$
52 fveq2 ${⊢}{k}={i}\to {G}\left({k}\right)={G}\left({i}\right)$
53 2fveq3 ${⊢}{k}={i}\to {F}\left({I}\left({k}\right)\right)={F}\left({I}\left({i}\right)\right)$
54 52 53 eqeq12d ${⊢}{k}={i}\to \left({G}\left({k}\right)={F}\left({I}\left({k}\right)\right)↔{G}\left({i}\right)={F}\left({I}\left({i}\right)\right)\right)$
55 51 54 imbi12d ${⊢}{k}={i}\to \left(\left(\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)={F}\left({I}\left({k}\right)\right)\right)↔\left(\left({\phi }\wedge {i}\in {Z}\right)\to {G}\left({i}\right)={F}\left({I}\left({i}\right)\right)\right)\right)$
56 49 55 13 chvarfv ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to {G}\left({i}\right)={F}\left({I}\left({i}\right)\right)$
57 5 eleq2i ${⊢}{i}\in {Z}↔{i}\in {ℤ}_{\ge {M}}$
58 57 biimpi ${⊢}{i}\in {Z}\to {i}\in {ℤ}_{\ge {M}}$
59 58 adantl ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to {i}\in {ℤ}_{\ge {M}}$
60 uzss ${⊢}{i}\in {ℤ}_{\ge {M}}\to {ℤ}_{\ge {i}}\subseteq {ℤ}_{\ge {M}}$
61 59 60 syl ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to {ℤ}_{\ge {i}}\subseteq {ℤ}_{\ge {M}}$
62 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({i}+1\right)$
63 4 62 nffv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{I}\left({i}+1\right)$
64 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{ℤ}_{\ge }$
65 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}+$
66 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}1$
67 46 65 66 nfov ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({I}\left({i}\right)+1\right)$
68 64 67 nffv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{ℤ}_{\ge \left({I}\left({i}\right)+1\right)}$
69 63 68 nfel ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{I}\left({i}+1\right)\in {ℤ}_{\ge \left({I}\left({i}\right)+1\right)}$
70 43 69 nfim ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {i}\in {Z}\right)\to {I}\left({i}+1\right)\in {ℤ}_{\ge \left({I}\left({i}\right)+1\right)}\right)$
71 fvoveq1 ${⊢}{k}={i}\to {I}\left({k}+1\right)={I}\left({i}+1\right)$
72 fveq2 ${⊢}{k}={i}\to {I}\left({k}\right)={I}\left({i}\right)$
73 72 fvoveq1d ${⊢}{k}={i}\to {ℤ}_{\ge \left({I}\left({k}\right)+1\right)}={ℤ}_{\ge \left({I}\left({i}\right)+1\right)}$
74 71 73 eleq12d ${⊢}{k}={i}\to \left({I}\left({k}+1\right)\in {ℤ}_{\ge \left({I}\left({k}\right)+1\right)}↔{I}\left({i}+1\right)\in {ℤ}_{\ge \left({I}\left({i}\right)+1\right)}\right)$
75 51 74 imbi12d ${⊢}{k}={i}\to \left(\left(\left({\phi }\wedge {k}\in {Z}\right)\to {I}\left({k}+1\right)\in {ℤ}_{\ge \left({I}\left({k}\right)+1\right)}\right)↔\left(\left({\phi }\wedge {i}\in {Z}\right)\to {I}\left({i}+1\right)\in {ℤ}_{\ge \left({I}\left({i}\right)+1\right)}\right)\right)$
76 70 75 11 chvarfv ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to {I}\left({i}+1\right)\in {ℤ}_{\ge \left({I}\left({i}\right)+1\right)}$
77 5 6 10 76 climsuselem1 ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to {I}\left({i}\right)\in {ℤ}_{\ge {i}}$
78 61 77 sseldd ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to {I}\left({i}\right)\in {ℤ}_{\ge {M}}$
79 78 5 eleqtrrdi ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to {I}\left({i}\right)\in {Z}$
80 79 ex ${⊢}{\phi }\to \left({i}\in {Z}\to {I}\left({i}\right)\in {Z}\right)$
81 80 imdistani ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to \left({\phi }\wedge {I}\left({i}\right)\in {Z}\right)$
82 42 nfci ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{Z}$
83 46 82 nfel ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{I}\left({i}\right)\in {Z}$
84 1 83 nfan ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {I}\left({i}\right)\in {Z}\right)$
85 47 nfel1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{F}\left({I}\left({i}\right)\right)\in ℂ$
86 84 85 nfim ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {I}\left({i}\right)\in {Z}\right)\to {F}\left({I}\left({i}\right)\right)\in ℂ\right)$
87 eleq1 ${⊢}{k}={I}\left({i}\right)\to \left({k}\in {Z}↔{I}\left({i}\right)\in {Z}\right)$
88 87 anbi2d ${⊢}{k}={I}\left({i}\right)\to \left(\left({\phi }\wedge {k}\in {Z}\right)↔\left({\phi }\wedge {I}\left({i}\right)\in {Z}\right)\right)$
89 fveq2 ${⊢}{k}={I}\left({i}\right)\to {F}\left({k}\right)={F}\left({I}\left({i}\right)\right)$
90 89 eleq1d ${⊢}{k}={I}\left({i}\right)\to \left({F}\left({k}\right)\in ℂ↔{F}\left({I}\left({i}\right)\right)\in ℂ\right)$
91 88 90 imbi12d ${⊢}{k}={I}\left({i}\right)\to \left(\left(\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in ℂ\right)↔\left(\left({\phi }\wedge {I}\left({i}\right)\in {Z}\right)\to {F}\left({I}\left({i}\right)\right)\in ℂ\right)\right)$
92 46 86 91 8 vtoclgf ${⊢}{I}\left({i}\right)\in {Z}\to \left(\left({\phi }\wedge {I}\left({i}\right)\in {Z}\right)\to {F}\left({I}\left({i}\right)\right)\in ℂ\right)$
93 79 81 92 sylc ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to {F}\left({I}\left({i}\right)\right)\in ℂ$
94 56 93 eqeltrd ${⊢}\left({\phi }\wedge {i}\in {Z}\right)\to {G}\left({i}\right)\in ℂ$
95 23 41 94 syl2anc ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {G}\left({i}\right)\in ℂ$
96 23 41 56 syl2anc ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {G}\left({i}\right)={F}\left({I}\left({i}\right)\right)$
97 96 fvoveq1d ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to \left|{G}\left({i}\right)-{A}\right|=\left|{F}\left({I}\left({i}\right)\right)-{A}\right|$
98 fveq2 ${⊢}{i}={h}\to {F}\left({i}\right)={F}\left({h}\right)$
99 98 eleq1d ${⊢}{i}={h}\to \left({F}\left({i}\right)\in ℂ↔{F}\left({h}\right)\in ℂ\right)$
100 98 fvoveq1d ${⊢}{i}={h}\to \left|{F}\left({i}\right)-{A}\right|=\left|{F}\left({h}\right)-{A}\right|$
101 100 breq1d ${⊢}{i}={h}\to \left(\left|{F}\left({i}\right)-{A}\right|<{x}↔\left|{F}\left({h}\right)-{A}\right|<{x}\right)$
102 99 101 anbi12d ${⊢}{i}={h}\to \left(\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)↔\left({F}\left({h}\right)\in ℂ\wedge \left|{F}\left({h}\right)-{A}\right|<{x}\right)\right)$
103 102 cbvralvw ${⊢}\forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)↔\forall {h}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({h}\right)\in ℂ\wedge \left|{F}\left({h}\right)-{A}\right|<{x}\right)$
104 103 biimpi ${⊢}\forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\to \forall {h}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({h}\right)\in ℂ\wedge \left|{F}\left({h}\right)-{A}\right|<{x}\right)$
105 104 ad2antlr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to \forall {h}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({h}\right)\in ℂ\wedge \left|{F}\left({h}\right)-{A}\right|<{x}\right)$
106 zre ${⊢}{j}\in ℤ\to {j}\in ℝ$
107 106 3ad2ant2 ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {j}\in ℝ$
108 simp3 ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}$
109 eluzelz ${⊢}{i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\to {i}\in ℤ$
110 zre ${⊢}{i}\in ℤ\to {i}\in ℝ$
111 108 109 110 3syl ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {i}\in ℝ$
112 simp1 ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {\phi }$
113 6 zred ${⊢}{\phi }\to {M}\in ℝ$
114 112 113 syl ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {M}\in ℝ$
115 simpl2 ${⊢}\left(\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\wedge {M}\le {j}\right)\to {j}\in ℤ$
116 115 zred ${⊢}\left(\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\wedge {M}\le {j}\right)\to {j}\in ℝ$
117 114 adantr ${⊢}\left(\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\wedge ¬{M}\le {j}\right)\to {M}\in ℝ$
118 116 117 ifclda ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to if\left({M}\le {j},{j},{M}\right)\in ℝ$
119 max1 ${⊢}\left({M}\in ℝ\wedge {j}\in ℝ\right)\to {M}\le if\left({M}\le {j},{j},{M}\right)$
120 114 107 119 syl2anc ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {M}\le if\left({M}\le {j},{j},{M}\right)$
121 eluzle ${⊢}{i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\to if\left({M}\le {j},{j},{M}\right)\le {i}$
122 121 3ad2ant3 ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to if\left({M}\le {j},{j},{M}\right)\le {i}$
123 114 118 111 120 122 letrd ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {M}\le {i}$
124 112 6 syl ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {M}\in ℤ$
125 109 3ad2ant3 ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {i}\in ℤ$
126 eluz ${⊢}\left({M}\in ℤ\wedge {i}\in ℤ\right)\to \left({i}\in {ℤ}_{\ge {M}}↔{M}\le {i}\right)$
127 124 125 126 syl2anc ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to \left({i}\in {ℤ}_{\ge {M}}↔{M}\le {i}\right)$
128 123 127 mpbird ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {i}\in {ℤ}_{\ge {M}}$
129 128 5 eleqtrrdi ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {i}\in {Z}$
130 112 129 jca ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to \left({\phi }\wedge {i}\in {Z}\right)$
131 eluzelre ${⊢}{I}\left({i}\right)\in {ℤ}_{\ge {M}}\to {I}\left({i}\right)\in ℝ$
132 130 78 131 3syl ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {I}\left({i}\right)\in ℝ$
133 max2 ${⊢}\left({M}\in ℝ\wedge {j}\in ℝ\right)\to {j}\le if\left({M}\le {j},{j},{M}\right)$
134 114 107 133 syl2anc ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {j}\le if\left({M}\le {j},{j},{M}\right)$
135 107 118 111 134 122 letrd ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {j}\le {i}$
136 eluzle ${⊢}{I}\left({i}\right)\in {ℤ}_{\ge {i}}\to {i}\le {I}\left({i}\right)$
137 130 77 136 3syl ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {i}\le {I}\left({i}\right)$
138 107 111 132 135 137 letrd ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {j}\le {I}\left({i}\right)$
139 simp2 ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {j}\in ℤ$
140 eluzelz ${⊢}{I}\left({i}\right)\in {ℤ}_{\ge {i}}\to {I}\left({i}\right)\in ℤ$
141 130 77 140 3syl ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {I}\left({i}\right)\in ℤ$
142 eluz ${⊢}\left({j}\in ℤ\wedge {I}\left({i}\right)\in ℤ\right)\to \left({I}\left({i}\right)\in {ℤ}_{\ge {j}}↔{j}\le {I}\left({i}\right)\right)$
143 139 141 142 syl2anc ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to \left({I}\left({i}\right)\in {ℤ}_{\ge {j}}↔{j}\le {I}\left({i}\right)\right)$
144 138 143 mpbird ${⊢}\left({\phi }\wedge {j}\in ℤ\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {I}\left({i}\right)\in {ℤ}_{\ge {j}}$
145 23 24 26 144 syl3anc ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to {I}\left({i}\right)\in {ℤ}_{\ge {j}}$
146 fveq2 ${⊢}{h}={I}\left({i}\right)\to {F}\left({h}\right)={F}\left({I}\left({i}\right)\right)$
147 146 eleq1d ${⊢}{h}={I}\left({i}\right)\to \left({F}\left({h}\right)\in ℂ↔{F}\left({I}\left({i}\right)\right)\in ℂ\right)$
148 146 fvoveq1d ${⊢}{h}={I}\left({i}\right)\to \left|{F}\left({h}\right)-{A}\right|=\left|{F}\left({I}\left({i}\right)\right)-{A}\right|$
149 148 breq1d ${⊢}{h}={I}\left({i}\right)\to \left(\left|{F}\left({h}\right)-{A}\right|<{x}↔\left|{F}\left({I}\left({i}\right)\right)-{A}\right|<{x}\right)$
150 147 149 anbi12d ${⊢}{h}={I}\left({i}\right)\to \left(\left({F}\left({h}\right)\in ℂ\wedge \left|{F}\left({h}\right)-{A}\right|<{x}\right)↔\left({F}\left({I}\left({i}\right)\right)\in ℂ\wedge \left|{F}\left({I}\left({i}\right)\right)-{A}\right|<{x}\right)\right)$
151 150 rspccva ${⊢}\left(\forall {h}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({h}\right)\in ℂ\wedge \left|{F}\left({h}\right)-{A}\right|<{x}\right)\wedge {I}\left({i}\right)\in {ℤ}_{\ge {j}}\right)\to \left({F}\left({I}\left({i}\right)\right)\in ℂ\wedge \left|{F}\left({I}\left({i}\right)\right)-{A}\right|<{x}\right)$
152 151 simprd ${⊢}\left(\forall {h}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({h}\right)\in ℂ\wedge \left|{F}\left({h}\right)-{A}\right|<{x}\right)\wedge {I}\left({i}\right)\in {ℤ}_{\ge {j}}\right)\to \left|{F}\left({I}\left({i}\right)\right)-{A}\right|<{x}$
153 105 145 152 syl2anc ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to \left|{F}\left({I}\left({i}\right)\right)-{A}\right|<{x}$
154 97 153 eqbrtrd ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to \left|{G}\left({i}\right)-{A}\right|<{x}$
155 95 154 jca ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\wedge {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\right)\to \left({G}\left({i}\right)\in ℂ\wedge \left|{G}\left({i}\right)-{A}\right|<{x}\right)$
156 155 ex ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\to \left({i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\to \left({G}\left({i}\right)\in ℂ\wedge \left|{G}\left({i}\right)-{A}\right|<{x}\right)\right)$
157 22 156 ralrimi ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\to \forall {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\phantom{\rule{.4em}{0ex}}\left({G}\left({i}\right)\in ℂ\wedge \left|{G}\left({i}\right)-{A}\right|<{x}\right)$
158 fveq2 ${⊢}{l}=if\left({M}\le {j},{j},{M}\right)\to {ℤ}_{\ge {l}}={ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}$
159 158 raleqdv ${⊢}{l}=if\left({M}\le {j},{j},{M}\right)\to \left(\forall {i}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}\left({G}\left({i}\right)\in ℂ\wedge \left|{G}\left({i}\right)-{A}\right|<{x}\right)↔\forall {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\phantom{\rule{.4em}{0ex}}\left({G}\left({i}\right)\in ℂ\wedge \left|{G}\left({i}\right)-{A}\right|<{x}\right)\right)$
160 159 rspcev ${⊢}\left(if\left({M}\le {j},{j},{M}\right)\in ℤ\wedge \forall {i}\in {ℤ}_{\ge if\left({M}\le {j},{j},{M}\right)}\phantom{\rule{.4em}{0ex}}\left({G}\left({i}\right)\in ℂ\wedge \left|{G}\left({i}\right)-{A}\right|<{x}\right)\right)\to \exists {l}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}\left({G}\left({i}\right)\in ℂ\wedge \left|{G}\left({i}\right)-{A}\right|<{x}\right)$
161 19 157 160 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\wedge {j}\in ℤ\right)\wedge \forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\to \exists {l}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}\left({G}\left({i}\right)\in ℂ\wedge \left|{G}\left({i}\right)-{A}\right|<{x}\right)$
162 eqidd ${⊢}\left({\phi }\wedge {i}\in ℤ\right)\to {F}\left({i}\right)={F}\left({i}\right)$
163 7 162 clim ${⊢}{\phi }\to \left({F}⇝{A}↔\left({A}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)\right)$
164 9 163 mpbid ${⊢}{\phi }\to \left({A}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)\right)$
165 164 simprd ${⊢}{\phi }\to \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)$
166 165 r19.21bi ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({F}\left({i}\right)\in ℂ\wedge \left|{F}\left({i}\right)-{A}\right|<{x}\right)$
167 161 166 r19.29a ${⊢}\left({\phi }\wedge {x}\in {ℝ}^{+}\right)\to \exists {l}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}\left({G}\left({i}\right)\in ℂ\wedge \left|{G}\left({i}\right)-{A}\right|<{x}\right)$
168 167 ex ${⊢}{\phi }\to \left({x}\in {ℝ}^{+}\to \exists {l}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}\left({G}\left({i}\right)\in ℂ\wedge \left|{G}\left({i}\right)-{A}\right|<{x}\right)\right)$
169 16 168 ralrimi ${⊢}{\phi }\to \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {l}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}\left({G}\left({i}\right)\in ℂ\wedge \left|{G}\left({i}\right)-{A}\right|<{x}\right)$
170 eqidd ${⊢}\left({\phi }\wedge {i}\in ℤ\right)\to {G}\left({i}\right)={G}\left({i}\right)$
171 12 170 clim ${⊢}{\phi }\to \left({G}⇝{A}↔\left({A}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {l}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {i}\in {ℤ}_{\ge {l}}\phantom{\rule{.4em}{0ex}}\left({G}\left({i}\right)\in ℂ\wedge \left|{G}\left({i}\right)-{A}\right|<{x}\right)\right)\right)$
172 15 169 171 mpbir2and ${⊢}{\phi }\to {G}⇝{A}$