# Metamath Proof Explorer

## Theorem mertenslem1

Description: Lemma for mertens . (Contributed by Mario Carneiro, 29-Apr-2014)

Ref Expression
Hypotheses mertens.1 ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {F}\left({j}\right)={A}$
mertens.2 ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {K}\left({j}\right)=\left|{A}\right|$
mertens.3 ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {A}\in ℂ$
mertens.4 ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {G}\left({k}\right)={B}$
mertens.5 ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {B}\in ℂ$
mertens.6 ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {H}\left({k}\right)=\sum _{{j}=0}^{{k}}{A}{G}\left({k}-{j}\right)$
mertens.7 ${⊢}{\phi }\to seq0\left(+,{K}\right)\in \mathrm{dom}⇝$
mertens.8 ${⊢}{\phi }\to seq0\left(+,{G}\right)\in \mathrm{dom}⇝$
mertens.9 ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
mertens.10 ${⊢}{T}=\left\{{z}|\exists {n}\in \left(0\dots {s}-1\right)\phantom{\rule{.4em}{0ex}}{z}=\left|\sum _{{k}\in {ℤ}_{\ge \left({n}+1\right)}}{G}\left({k}\right)\right|\right\}$
mertens.11 ${⊢}{\psi }↔\left({s}\in ℕ\wedge \forall {n}\in {ℤ}_{\ge {s}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{k}\in {ℤ}_{\ge \left({n}+1\right)}}{G}\left({k}\right)\right|<\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\right)$
mertens.12 ${⊢}{\phi }\to \left({\psi }\wedge \left({t}\in {ℕ}_{0}\wedge \forall {m}\in {ℤ}_{\ge {t}}\phantom{\rule{.4em}{0ex}}{K}\left({m}\right)<\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)\right)$
mertens.13 ${⊢}{\phi }\to \left(0\le sup\left({T},ℝ,<\right)\wedge \left({T}\subseteq ℝ\wedge {T}\ne \varnothing \wedge \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in {T}\phantom{\rule{.4em}{0ex}}{w}\le {z}\right)\right)$
Assertion mertenslem1 ${⊢}{\phi }\to \exists {y}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {y}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{j}=0}^{{m}}{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|<{E}$

### Proof

Step Hyp Ref Expression
1 mertens.1 ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {F}\left({j}\right)={A}$
2 mertens.2 ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {K}\left({j}\right)=\left|{A}\right|$
3 mertens.3 ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {A}\in ℂ$
4 mertens.4 ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {G}\left({k}\right)={B}$
5 mertens.5 ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {B}\in ℂ$
6 mertens.6 ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {H}\left({k}\right)=\sum _{{j}=0}^{{k}}{A}{G}\left({k}-{j}\right)$
7 mertens.7 ${⊢}{\phi }\to seq0\left(+,{K}\right)\in \mathrm{dom}⇝$
8 mertens.8 ${⊢}{\phi }\to seq0\left(+,{G}\right)\in \mathrm{dom}⇝$
9 mertens.9 ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
10 mertens.10 ${⊢}{T}=\left\{{z}|\exists {n}\in \left(0\dots {s}-1\right)\phantom{\rule{.4em}{0ex}}{z}=\left|\sum _{{k}\in {ℤ}_{\ge \left({n}+1\right)}}{G}\left({k}\right)\right|\right\}$
11 mertens.11 ${⊢}{\psi }↔\left({s}\in ℕ\wedge \forall {n}\in {ℤ}_{\ge {s}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{k}\in {ℤ}_{\ge \left({n}+1\right)}}{G}\left({k}\right)\right|<\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\right)$
12 mertens.12 ${⊢}{\phi }\to \left({\psi }\wedge \left({t}\in {ℕ}_{0}\wedge \forall {m}\in {ℤ}_{\ge {t}}\phantom{\rule{.4em}{0ex}}{K}\left({m}\right)<\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)\right)$
13 mertens.13 ${⊢}{\phi }\to \left(0\le sup\left({T},ℝ,<\right)\wedge \left({T}\subseteq ℝ\wedge {T}\ne \varnothing \wedge \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in {T}\phantom{\rule{.4em}{0ex}}{w}\le {z}\right)\right)$
14 12 simpld ${⊢}{\phi }\to {\psi }$
15 14 11 sylib ${⊢}{\phi }\to \left({s}\in ℕ\wedge \forall {n}\in {ℤ}_{\ge {s}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{k}\in {ℤ}_{\ge \left({n}+1\right)}}{G}\left({k}\right)\right|<\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\right)$
16 15 simpld ${⊢}{\phi }\to {s}\in ℕ$
17 16 nnnn0d ${⊢}{\phi }\to {s}\in {ℕ}_{0}$
18 12 simprd ${⊢}{\phi }\to \left({t}\in {ℕ}_{0}\wedge \forall {m}\in {ℤ}_{\ge {t}}\phantom{\rule{.4em}{0ex}}{K}\left({m}\right)<\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)$
19 18 simpld ${⊢}{\phi }\to {t}\in {ℕ}_{0}$
20 17 19 nn0addcld ${⊢}{\phi }\to {s}+{t}\in {ℕ}_{0}$
21 fzfid ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(0\dots {m}\right)\in \mathrm{Fin}$
22 simpl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {\phi }$
23 elfznn0 ${⊢}{j}\in \left(0\dots {m}\right)\to {j}\in {ℕ}_{0}$
24 22 23 3 syl2an ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\to {A}\in ℂ$
25 eqid ${⊢}{ℤ}_{\ge \left({m}-{j}+1\right)}={ℤ}_{\ge \left({m}-{j}+1\right)}$
26 fznn0sub ${⊢}{j}\in \left(0\dots {m}\right)\to {m}-{j}\in {ℕ}_{0}$
27 26 adantl ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\to {m}-{j}\in {ℕ}_{0}$
28 peano2nn0 ${⊢}{m}-{j}\in {ℕ}_{0}\to {m}-{j}+1\in {ℕ}_{0}$
29 27 28 syl ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\to {m}-{j}+1\in {ℕ}_{0}$
30 29 nn0zd ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\to {m}-{j}+1\in ℤ$
31 simplll ${⊢}\left(\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\wedge {k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}\right)\to {\phi }$
32 eluznn0 ${⊢}\left({m}-{j}+1\in {ℕ}_{0}\wedge {k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}\right)\to {k}\in {ℕ}_{0}$
33 29 32 sylan ${⊢}\left(\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\wedge {k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}\right)\to {k}\in {ℕ}_{0}$
34 31 33 4 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\wedge {k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}\right)\to {G}\left({k}\right)={B}$
35 31 33 5 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\wedge {k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}\right)\to {B}\in ℂ$
36 8 ad2antrr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\to seq0\left(+,{G}\right)\in \mathrm{dom}⇝$
37 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
38 simpll ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\to {\phi }$
39 4 5 eqeltrd ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {G}\left({k}\right)\in ℂ$
40 38 39 sylan ${⊢}\left(\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {G}\left({k}\right)\in ℂ$
41 37 29 40 iserex ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\to \left(seq0\left(+,{G}\right)\in \mathrm{dom}⇝↔seq\left({m}-{j}+1\right)\left(+,{G}\right)\in \mathrm{dom}⇝\right)$
42 36 41 mpbid ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\to seq\left({m}-{j}+1\right)\left(+,{G}\right)\in \mathrm{dom}⇝$
43 25 30 34 35 42 isumcl ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\to \sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\in ℂ$
44 24 43 mulcld ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\to {A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\in ℂ$
45 21 44 fsumcl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}}{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\in ℂ$
46 45 abscld ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left|\sum _{{j}=0}^{{m}}{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in ℝ$
47 44 abscld ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\to \left|{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in ℝ$
48 21 47 fsumrecl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}}\left|{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in ℝ$
49 9 rpred ${⊢}{\phi }\to {E}\in ℝ$
50 49 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {E}\in ℝ$
51 21 44 fsumabs ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left|\sum _{{j}=0}^{{m}}{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\le \sum _{{j}=0}^{{m}}\left|{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|$
52 fzfid ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(0\dots {m}-{s}\right)\in \mathrm{Fin}$
53 17 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {s}\in {ℕ}_{0}$
54 53 nn0ge0d ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to 0\le {s}$
55 eluzelz ${⊢}{m}\in {ℤ}_{\ge \left({s}+{t}\right)}\to {m}\in ℤ$
56 55 adantl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}\in ℤ$
57 56 zred ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}\in ℝ$
58 53 nn0red ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {s}\in ℝ$
59 57 58 subge02d ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(0\le {s}↔{m}-{s}\le {m}\right)$
60 54 59 mpbid ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}-{s}\le {m}$
61 53 37 eleqtrdi ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {s}\in {ℤ}_{\ge 0}$
62 16 nnzd ${⊢}{\phi }\to {s}\in ℤ$
63 uzid ${⊢}{s}\in ℤ\to {s}\in {ℤ}_{\ge {s}}$
64 62 63 syl ${⊢}{\phi }\to {s}\in {ℤ}_{\ge {s}}$
65 uzaddcl ${⊢}\left({s}\in {ℤ}_{\ge {s}}\wedge {t}\in {ℕ}_{0}\right)\to {s}+{t}\in {ℤ}_{\ge {s}}$
66 64 19 65 syl2anc ${⊢}{\phi }\to {s}+{t}\in {ℤ}_{\ge {s}}$
67 eqid ${⊢}{ℤ}_{\ge {s}}={ℤ}_{\ge {s}}$
68 67 uztrn2 ${⊢}\left({s}+{t}\in {ℤ}_{\ge {s}}\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}\in {ℤ}_{\ge {s}}$
69 66 68 sylan ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}\in {ℤ}_{\ge {s}}$
70 elfzuzb ${⊢}{s}\in \left(0\dots {m}\right)↔\left({s}\in {ℤ}_{\ge 0}\wedge {m}\in {ℤ}_{\ge {s}}\right)$
71 61 69 70 sylanbrc ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {s}\in \left(0\dots {m}\right)$
72 fznn0sub2 ${⊢}{s}\in \left(0\dots {m}\right)\to {m}-{s}\in \left(0\dots {m}\right)$
73 71 72 syl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}-{s}\in \left(0\dots {m}\right)$
74 elfzelz ${⊢}{m}-{s}\in \left(0\dots {m}\right)\to {m}-{s}\in ℤ$
75 73 74 syl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}-{s}\in ℤ$
76 eluz ${⊢}\left({m}-{s}\in ℤ\wedge {m}\in ℤ\right)\to \left({m}\in {ℤ}_{\ge \left({m}-{s}\right)}↔{m}-{s}\le {m}\right)$
77 75 56 76 syl2anc ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left({m}\in {ℤ}_{\ge \left({m}-{s}\right)}↔{m}-{s}\le {m}\right)$
78 60 77 mpbird ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}\in {ℤ}_{\ge \left({m}-{s}\right)}$
79 fzss2 ${⊢}{m}\in {ℤ}_{\ge \left({m}-{s}\right)}\to \left(0\dots {m}-{s}\right)\subseteq \left(0\dots {m}\right)$
80 78 79 syl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(0\dots {m}-{s}\right)\subseteq \left(0\dots {m}\right)$
81 80 sselda ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to {j}\in \left(0\dots {m}\right)$
82 3 abscld ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \left|{A}\right|\in ℝ$
83 22 23 82 syl2an ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\to \left|{A}\right|\in ℝ$
84 43 abscld ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\to \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in ℝ$
85 83 84 remulcld ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\to \left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in ℝ$
86 81 85 syldan ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to \left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in ℝ$
87 52 86 fsumrecl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in ℝ$
88 fzfid ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left({m}-{s}+1\dots {m}\right)\in \mathrm{Fin}$
89 elfznn0 ${⊢}{m}-{s}\in \left(0\dots {m}\right)\to {m}-{s}\in {ℕ}_{0}$
90 73 89 syl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}-{s}\in {ℕ}_{0}$
91 peano2nn0 ${⊢}{m}-{s}\in {ℕ}_{0}\to {m}-{s}+1\in {ℕ}_{0}$
92 90 91 syl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}-{s}+1\in {ℕ}_{0}$
93 92 37 eleqtrdi ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}-{s}+1\in {ℤ}_{\ge 0}$
94 fzss1 ${⊢}{m}-{s}+1\in {ℤ}_{\ge 0}\to \left({m}-{s}+1\dots {m}\right)\subseteq \left(0\dots {m}\right)$
95 93 94 syl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left({m}-{s}+1\dots {m}\right)\subseteq \left(0\dots {m}\right)$
96 95 sselda ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {j}\in \left(0\dots {m}\right)$
97 96 85 syldan ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in ℝ$
98 88 97 fsumrecl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}={m}-{s}+1}^{{m}}\left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in ℝ$
99 9 rphalfcld ${⊢}{\phi }\to \frac{{E}}{2}\in {ℝ}^{+}$
100 99 rpred ${⊢}{\phi }\to \frac{{E}}{2}\in ℝ$
101 100 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \frac{{E}}{2}\in ℝ$
102 elfznn0 ${⊢}{j}\in \left(0\dots {m}-{s}\right)\to {j}\in {ℕ}_{0}$
103 22 102 82 syl2an ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to \left|{A}\right|\in ℝ$
104 52 103 fsumrecl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\in ℝ$
105 104 101 remulcld ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{{E}}{2}\right)\in ℝ$
106 0zd ${⊢}{\phi }\to 0\in ℤ$
107 eqidd ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {K}\left({j}\right)={K}\left({j}\right)$
108 2 82 eqeltrd ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {K}\left({j}\right)\in ℝ$
109 37 106 107 108 7 isumrecl ${⊢}{\phi }\to \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)\in ℝ$
110 3 absge0d ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to 0\le \left|{A}\right|$
111 110 2 breqtrrd ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to 0\le {K}\left({j}\right)$
112 37 106 107 108 7 111 isumge0 ${⊢}{\phi }\to 0\le \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)$
113 109 112 ge0p1rpd ${⊢}{\phi }\to \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\in {ℝ}^{+}$
114 113 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\in {ℝ}^{+}$
115 105 114 rerpdivcld ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \frac{\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{{E}}{2}\right)}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\in ℝ$
116 99 113 rpdivcld ${⊢}{\phi }\to \frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\in {ℝ}^{+}$
117 116 rpred ${⊢}{\phi }\to \frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\in ℝ$
118 117 ad2antrr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to \frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\in ℝ$
119 103 118 remulcld ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to \left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\right)\in ℝ$
120 81 30 syldan ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to {m}-{j}+1\in ℤ$
121 simplll ${⊢}\left(\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\wedge {k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}\right)\to {\phi }$
122 81 29 syldan ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to {m}-{j}+1\in {ℕ}_{0}$
123 122 32 sylan ${⊢}\left(\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\wedge {k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}\right)\to {k}\in {ℕ}_{0}$
124 121 123 4 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\wedge {k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}\right)\to {G}\left({k}\right)={B}$
125 121 123 5 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\wedge {k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}\right)\to {B}\in ℂ$
126 81 42 syldan ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to seq\left({m}-{j}+1\right)\left(+,{G}\right)\in \mathrm{dom}⇝$
127 25 120 124 125 126 isumcl ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to \sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\in ℂ$
128 127 abscld ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in ℝ$
129 82 110 jca ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \left(\left|{A}\right|\in ℝ\wedge 0\le \left|{A}\right|\right)$
130 22 102 129 syl2an ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to \left(\left|{A}\right|\in ℝ\wedge 0\le \left|{A}\right|\right)$
131 124 sumeq2dv ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to \sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{G}\left({k}\right)=\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}$
132 131 fveq2d ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{G}\left({k}\right)\right|=\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|$
133 fvoveq1 ${⊢}{n}={m}-{j}\to {ℤ}_{\ge \left({n}+1\right)}={ℤ}_{\ge \left({m}-{j}+1\right)}$
134 133 sumeq1d ${⊢}{n}={m}-{j}\to \sum _{{k}\in {ℤ}_{\ge \left({n}+1\right)}}{G}\left({k}\right)=\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{G}\left({k}\right)$
135 134 fveq2d ${⊢}{n}={m}-{j}\to \left|\sum _{{k}\in {ℤ}_{\ge \left({n}+1\right)}}{G}\left({k}\right)\right|=\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{G}\left({k}\right)\right|$
136 135 breq1d ${⊢}{n}={m}-{j}\to \left(\left|\sum _{{k}\in {ℤ}_{\ge \left({n}+1\right)}}{G}\left({k}\right)\right|<\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}↔\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{G}\left({k}\right)\right|<\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\right)$
137 15 simprd ${⊢}{\phi }\to \forall {n}\in {ℤ}_{\ge {s}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{k}\in {ℤ}_{\ge \left({n}+1\right)}}{G}\left({k}\right)\right|<\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}$
138 137 ad2antrr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to \forall {n}\in {ℤ}_{\ge {s}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{k}\in {ℤ}_{\ge \left({n}+1\right)}}{G}\left({k}\right)\right|<\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}$
139 elfzelz ${⊢}{j}\in \left(0\dots {m}-{s}\right)\to {j}\in ℤ$
140 139 adantl ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to {j}\in ℤ$
141 140 zred ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to {j}\in ℝ$
142 55 ad2antlr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to {m}\in ℤ$
143 142 zred ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to {m}\in ℝ$
144 62 ad2antrr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to {s}\in ℤ$
145 144 zred ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to {s}\in ℝ$
146 elfzle2 ${⊢}{j}\in \left(0\dots {m}-{s}\right)\to {j}\le {m}-{s}$
147 146 adantl ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to {j}\le {m}-{s}$
148 141 143 145 147 lesubd ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to {s}\le {m}-{j}$
149 142 140 zsubcld ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to {m}-{j}\in ℤ$
150 eluz ${⊢}\left({s}\in ℤ\wedge {m}-{j}\in ℤ\right)\to \left({m}-{j}\in {ℤ}_{\ge {s}}↔{s}\le {m}-{j}\right)$
151 144 149 150 syl2anc ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to \left({m}-{j}\in {ℤ}_{\ge {s}}↔{s}\le {m}-{j}\right)$
152 148 151 mpbird ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to {m}-{j}\in {ℤ}_{\ge {s}}$
153 136 138 152 rspcdva ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{G}\left({k}\right)\right|<\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}$
154 132 153 eqbrtrrd ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|<\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}$
155 128 118 154 ltled ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\le \frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}$
156 lemul2a ${⊢}\left(\left(\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in ℝ\wedge \frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\in ℝ\wedge \left(\left|{A}\right|\in ℝ\wedge 0\le \left|{A}\right|\right)\right)\wedge \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\le \frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\right)\to \left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\le \left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\right)$
157 128 118 130 155 156 syl31anc ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to \left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\le \left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\right)$
158 52 86 119 157 fsumle ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\le \sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\right)$
159 104 recnd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\in ℂ$
160 99 rpcnd ${⊢}{\phi }\to \frac{{E}}{2}\in ℂ$
161 160 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \frac{{E}}{2}\in ℂ$
162 peano2re ${⊢}\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)\in ℝ\to \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\in ℝ$
163 109 162 syl ${⊢}{\phi }\to \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\in ℝ$
164 163 recnd ${⊢}{\phi }\to \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\in ℂ$
165 164 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\in ℂ$
166 113 rpne0d ${⊢}{\phi }\to \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\ne 0$
167 166 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\ne 0$
168 159 161 165 167 divassd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \frac{\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{{E}}{2}\right)}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}=\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\right)$
169 fveq2 ${⊢}{n}={j}\to {K}\left({n}\right)={K}\left({j}\right)$
170 169 cbvsumv ${⊢}\sum _{{n}\in {ℕ}_{0}}{K}\left({n}\right)=\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)$
171 170 oveq1i ${⊢}\sum _{{n}\in {ℕ}_{0}}{K}\left({n}\right)+1=\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1$
172 171 oveq2i ${⊢}\frac{\frac{{E}}{2}}{\sum _{{n}\in {ℕ}_{0}}{K}\left({n}\right)+1}=\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}$
173 172 116 eqeltrid ${⊢}{\phi }\to \frac{\frac{{E}}{2}}{\sum _{{n}\in {ℕ}_{0}}{K}\left({n}\right)+1}\in {ℝ}^{+}$
174 173 rpcnd ${⊢}{\phi }\to \frac{\frac{{E}}{2}}{\sum _{{n}\in {ℕ}_{0}}{K}\left({n}\right)+1}\in ℂ$
175 174 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \frac{\frac{{E}}{2}}{\sum _{{n}\in {ℕ}_{0}}{K}\left({n}\right)+1}\in ℂ$
176 82 recnd ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \left|{A}\right|\in ℂ$
177 22 102 176 syl2an ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}-{s}\right)\right)\to \left|{A}\right|\in ℂ$
178 52 175 177 fsummulc1 ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{n}\in {ℕ}_{0}}{K}\left({n}\right)+1}\right)=\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{n}\in {ℕ}_{0}}{K}\left({n}\right)+1}\right)$
179 172 oveq2i ${⊢}\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{n}\in {ℕ}_{0}}{K}\left({n}\right)+1}\right)=\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\right)$
180 172 oveq2i ${⊢}\left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{n}\in {ℕ}_{0}}{K}\left({n}\right)+1}\right)=\left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\right)$
181 180 a1i ${⊢}{j}\in \left(0\dots {m}-{s}\right)\to \left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{n}\in {ℕ}_{0}}{K}\left({n}\right)+1}\right)=\left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\right)$
182 181 sumeq2i ${⊢}\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{n}\in {ℕ}_{0}}{K}\left({n}\right)+1}\right)=\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\right)$
183 178 179 182 3eqtr3g ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\right)=\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\right)$
184 168 183 eqtrd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \frac{\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{{E}}{2}\right)}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}=\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{\frac{{E}}{2}}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}\right)$
185 158 184 breqtrrd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\le \frac{\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{{E}}{2}\right)}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}$
186 109 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)\in ℝ$
187 163 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\in ℝ$
188 0zd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to 0\in ℤ$
189 fz0ssnn0 ${⊢}\left(0\dots {m}-{s}\right)\subseteq {ℕ}_{0}$
190 189 a1i ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(0\dots {m}-{s}\right)\subseteq {ℕ}_{0}$
191 2 adantlr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in {ℕ}_{0}\right)\to {K}\left({j}\right)=\left|{A}\right|$
192 82 adantlr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in {ℕ}_{0}\right)\to \left|{A}\right|\in ℝ$
193 110 adantlr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in {ℕ}_{0}\right)\to 0\le \left|{A}\right|$
194 7 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to seq0\left(+,{K}\right)\in \mathrm{dom}⇝$
195 37 188 52 190 191 192 193 194 isumless ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\le \sum _{{j}\in {ℕ}_{0}}\left|{A}\right|$
196 2 sumeq2dv ${⊢}{\phi }\to \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)=\sum _{{j}\in {ℕ}_{0}}\left|{A}\right|$
197 196 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)=\sum _{{j}\in {ℕ}_{0}}\left|{A}\right|$
198 195 197 breqtrrd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\le \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)$
199 109 ltp1d ${⊢}{\phi }\to \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)<\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1$
200 199 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)<\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1$
201 104 186 187 198 200 lelttrd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}-{s}}\left|{A}\right|<\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1$
202 99 rpregt0d ${⊢}{\phi }\to \left(\frac{{E}}{2}\in ℝ\wedge 0<\frac{{E}}{2}\right)$
203 202 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(\frac{{E}}{2}\in ℝ\wedge 0<\frac{{E}}{2}\right)$
204 ltmul1 ${⊢}\left(\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\in ℝ\wedge \sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\in ℝ\wedge \left(\frac{{E}}{2}\in ℝ\wedge 0<\frac{{E}}{2}\right)\right)\to \left(\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|<\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1↔\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{{E}}{2}\right)<\left(\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\right)\left(\frac{{E}}{2}\right)\right)$
205 104 187 203 204 syl3anc ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|<\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1↔\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{{E}}{2}\right)<\left(\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\right)\left(\frac{{E}}{2}\right)\right)$
206 201 205 mpbid ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{{E}}{2}\right)<\left(\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\right)\left(\frac{{E}}{2}\right)$
207 113 rpregt0d ${⊢}{\phi }\to \left(\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\in ℝ\wedge 0<\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\right)$
208 207 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\in ℝ\wedge 0<\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\right)$
209 ltdivmul ${⊢}\left(\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{{E}}{2}\right)\in ℝ\wedge \frac{{E}}{2}\in ℝ\wedge \left(\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\in ℝ\wedge 0<\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\right)\right)\to \left(\frac{\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{{E}}{2}\right)}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}<\frac{{E}}{2}↔\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{{E}}{2}\right)<\left(\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\right)\left(\frac{{E}}{2}\right)\right)$
210 105 101 208 209 syl3anc ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(\frac{\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{{E}}{2}\right)}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}<\frac{{E}}{2}↔\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{{E}}{2}\right)<\left(\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1\right)\left(\frac{{E}}{2}\right)\right)$
211 206 210 mpbird ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \frac{\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left(\frac{{E}}{2}\right)}{\sum _{{j}\in {ℕ}_{0}}{K}\left({j}\right)+1}<\frac{{E}}{2}$
212 87 115 101 185 211 lelttrd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|<\frac{{E}}{2}$
213 13 simprd ${⊢}{\phi }\to \left({T}\subseteq ℝ\wedge {T}\ne \varnothing \wedge \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in {T}\phantom{\rule{.4em}{0ex}}{w}\le {z}\right)$
214 suprcl ${⊢}\left({T}\subseteq ℝ\wedge {T}\ne \varnothing \wedge \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in {T}\phantom{\rule{.4em}{0ex}}{w}\le {z}\right)\to sup\left({T},ℝ,<\right)\in ℝ$
215 213 214 syl ${⊢}{\phi }\to sup\left({T},ℝ,<\right)\in ℝ$
216 100 215 remulcld ${⊢}{\phi }\to \left(\frac{{E}}{2}\right)sup\left({T},ℝ,<\right)\in ℝ$
217 13 simpld ${⊢}{\phi }\to 0\le sup\left({T},ℝ,<\right)$
218 215 217 ge0p1rpd ${⊢}{\phi }\to sup\left({T},ℝ,<\right)+1\in {ℝ}^{+}$
219 216 218 rerpdivcld ${⊢}{\phi }\to \frac{\left(\frac{{E}}{2}\right)sup\left({T},ℝ,<\right)}{sup\left({T},ℝ,<\right)+1}\in ℝ$
220 219 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \frac{\left(\frac{{E}}{2}\right)sup\left({T},ℝ,<\right)}{sup\left({T},ℝ,<\right)+1}\in ℝ$
221 16 nnrpd ${⊢}{\phi }\to {s}\in {ℝ}^{+}$
222 99 221 rpdivcld ${⊢}{\phi }\to \frac{\frac{{E}}{2}}{{s}}\in {ℝ}^{+}$
223 222 218 rpdivcld ${⊢}{\phi }\to \frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\in {ℝ}^{+}$
224 223 rpred ${⊢}{\phi }\to \frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\in ℝ$
225 224 215 remulcld ${⊢}{\phi }\to \left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)\in ℝ$
226 225 ad2antrr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)\in ℝ$
227 simpll ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {\phi }$
228 96 23 syl ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {j}\in {ℕ}_{0}$
229 227 228 82 syl2anc ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \left|{A}\right|\in ℝ$
230 224 ad2antrr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\in ℝ$
231 227 228 2 syl2anc ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {K}\left({j}\right)=\left|{A}\right|$
232 fveq2 ${⊢}{m}={j}\to {K}\left({m}\right)={K}\left({j}\right)$
233 232 breq1d ${⊢}{m}={j}\to \left({K}\left({m}\right)<\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}↔{K}\left({j}\right)<\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)$
234 18 simprd ${⊢}{\phi }\to \forall {m}\in {ℤ}_{\ge {t}}\phantom{\rule{.4em}{0ex}}{K}\left({m}\right)<\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}$
235 234 ad2antrr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \forall {m}\in {ℤ}_{\ge {t}}\phantom{\rule{.4em}{0ex}}{K}\left({m}\right)<\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}$
236 elfzuz ${⊢}{j}\in \left({m}-{s}+1\dots {m}\right)\to {j}\in {ℤ}_{\ge \left({m}-{s}+1\right)}$
237 eluzle ${⊢}{m}\in {ℤ}_{\ge \left({s}+{t}\right)}\to {s}+{t}\le {m}$
238 237 adantl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {s}+{t}\le {m}$
239 19 nn0zd ${⊢}{\phi }\to {t}\in ℤ$
240 239 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {t}\in ℤ$
241 240 zred ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {t}\in ℝ$
242 58 241 57 leaddsub2d ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left({s}+{t}\le {m}↔{t}\le {m}-{s}\right)$
243 238 242 mpbid ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {t}\le {m}-{s}$
244 eluz ${⊢}\left({t}\in ℤ\wedge {m}-{s}\in ℤ\right)\to \left({m}-{s}\in {ℤ}_{\ge {t}}↔{t}\le {m}-{s}\right)$
245 240 75 244 syl2anc ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left({m}-{s}\in {ℤ}_{\ge {t}}↔{t}\le {m}-{s}\right)$
246 243 245 mpbird ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}-{s}\in {ℤ}_{\ge {t}}$
247 peano2uz ${⊢}{m}-{s}\in {ℤ}_{\ge {t}}\to {m}-{s}+1\in {ℤ}_{\ge {t}}$
248 246 247 syl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}-{s}+1\in {ℤ}_{\ge {t}}$
249 uztrn ${⊢}\left({j}\in {ℤ}_{\ge \left({m}-{s}+1\right)}\wedge {m}-{s}+1\in {ℤ}_{\ge {t}}\right)\to {j}\in {ℤ}_{\ge {t}}$
250 236 248 249 syl2anr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {j}\in {ℤ}_{\ge {t}}$
251 233 235 250 rspcdva ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {K}\left({j}\right)<\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}$
252 231 251 eqbrtrrd ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \left|{A}\right|<\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}$
253 229 230 252 ltled ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \left|{A}\right|\le \frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}$
254 213 ad2antrr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \left({T}\subseteq ℝ\wedge {T}\ne \varnothing \wedge \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in {T}\phantom{\rule{.4em}{0ex}}{w}\le {z}\right)$
255 57 adantr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {m}\in ℝ$
256 peano2zm ${⊢}{s}\in ℤ\to {s}-1\in ℤ$
257 62 256 syl ${⊢}{\phi }\to {s}-1\in ℤ$
258 257 zred ${⊢}{\phi }\to {s}-1\in ℝ$
259 258 ad2antrr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {s}-1\in ℝ$
260 228 nn0red ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {j}\in ℝ$
261 56 zcnd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}\in ℂ$
262 58 recnd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {s}\in ℂ$
263 1cnd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to 1\in ℂ$
264 261 262 263 subsubd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}-\left({s}-1\right)={m}-{s}+1$
265 264 adantr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {m}-\left({s}-1\right)={m}-{s}+1$
266 elfzle1 ${⊢}{j}\in \left({m}-{s}+1\dots {m}\right)\to {m}-{s}+1\le {j}$
267 266 adantl ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {m}-{s}+1\le {j}$
268 265 267 eqbrtrd ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {m}-\left({s}-1\right)\le {j}$
269 255 259 260 268 subled ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {m}-{j}\le {s}-1$
270 96 26 syl ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {m}-{j}\in {ℕ}_{0}$
271 270 37 eleqtrdi ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {m}-{j}\in {ℤ}_{\ge 0}$
272 257 ad2antrr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {s}-1\in ℤ$
273 elfz5 ${⊢}\left({m}-{j}\in {ℤ}_{\ge 0}\wedge {s}-1\in ℤ\right)\to \left({m}-{j}\in \left(0\dots {s}-1\right)↔{m}-{j}\le {s}-1\right)$
274 271 272 273 syl2anc ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \left({m}-{j}\in \left(0\dots {s}-1\right)↔{m}-{j}\le {s}-1\right)$
275 269 274 mpbird ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {m}-{j}\in \left(0\dots {s}-1\right)$
276 simplll ${⊢}\left(\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\wedge {k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}\right)\to {\phi }$
277 96 29 syldan ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to {m}-{j}+1\in {ℕ}_{0}$
278 277 32 sylan ${⊢}\left(\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\wedge {k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}\right)\to {k}\in {ℕ}_{0}$
279 276 278 4 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\wedge {k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}\right)\to {G}\left({k}\right)={B}$
280 279 sumeq2dv ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{G}\left({k}\right)=\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}$
281 280 eqcomd ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}=\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{G}\left({k}\right)$
282 281 fveq2d ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|=\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{G}\left({k}\right)\right|$
283 135 rspceeqv ${⊢}\left({m}-{j}\in \left(0\dots {s}-1\right)\wedge \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|=\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{G}\left({k}\right)\right|\right)\to \exists {n}\in \left(0\dots {s}-1\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|=\left|\sum _{{k}\in {ℤ}_{\ge \left({n}+1\right)}}{G}\left({k}\right)\right|$
284 275 282 283 syl2anc ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \exists {n}\in \left(0\dots {s}-1\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|=\left|\sum _{{k}\in {ℤ}_{\ge \left({n}+1\right)}}{G}\left({k}\right)\right|$
285 fvex ${⊢}\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in \mathrm{V}$
286 eqeq1 ${⊢}{z}=\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\to \left({z}=\left|\sum _{{k}\in {ℤ}_{\ge \left({n}+1\right)}}{G}\left({k}\right)\right|↔\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|=\left|\sum _{{k}\in {ℤ}_{\ge \left({n}+1\right)}}{G}\left({k}\right)\right|\right)$
287 286 rexbidv ${⊢}{z}=\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\to \left(\exists {n}\in \left(0\dots {s}-1\right)\phantom{\rule{.4em}{0ex}}{z}=\left|\sum _{{k}\in {ℤ}_{\ge \left({n}+1\right)}}{G}\left({k}\right)\right|↔\exists {n}\in \left(0\dots {s}-1\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|=\left|\sum _{{k}\in {ℤ}_{\ge \left({n}+1\right)}}{G}\left({k}\right)\right|\right)$
288 285 287 10 elab2 ${⊢}\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in {T}↔\exists {n}\in \left(0\dots {s}-1\right)\phantom{\rule{.4em}{0ex}}\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|=\left|\sum _{{k}\in {ℤ}_{\ge \left({n}+1\right)}}{G}\left({k}\right)\right|$
289 284 288 sylibr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in {T}$
290 suprub ${⊢}\left(\left({T}\subseteq ℝ\wedge {T}\ne \varnothing \wedge \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {w}\in {T}\phantom{\rule{.4em}{0ex}}{w}\le {z}\right)\wedge \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in {T}\right)\to \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\le sup\left({T},ℝ,<\right)$
291 254 289 290 syl2anc ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\le sup\left({T},ℝ,<\right)$
292 227 228 129 syl2anc ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \left(\left|{A}\right|\in ℝ\wedge 0\le \left|{A}\right|\right)$
293 96 84 syldan ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in ℝ$
294 43 absge0d ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\to 0\le \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|$
295 96 294 syldan ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to 0\le \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|$
296 293 295 jca ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \left(\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in ℝ\wedge 0\le \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\right)$
297 215 ad2antrr ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to sup\left({T},ℝ,<\right)\in ℝ$
298 lemul12a ${⊢}\left(\left(\left(\left|{A}\right|\in ℝ\wedge 0\le \left|{A}\right|\right)\wedge \frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\in ℝ\right)\wedge \left(\left(\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in ℝ\wedge 0\le \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\right)\wedge sup\left({T},ℝ,<\right)\in ℝ\right)\right)\to \left(\left(\left|{A}\right|\le \frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\wedge \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\le sup\left({T},ℝ,<\right)\right)\to \left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\le \left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)\right)$
299 292 230 296 297 298 syl22anc ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \left(\left(\left|{A}\right|\le \frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\wedge \left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\le sup\left({T},ℝ,<\right)\right)\to \left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\le \left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)\right)$
300 253 291 299 mp2and ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left({m}-{s}+1\dots {m}\right)\right)\to \left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\le \left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)$
301 88 97 226 300 fsumle ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}={m}-{s}+1}^{{m}}\left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\le \sum _{{j}={m}-{s}+1}^{{m}}\left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)$
302 225 recnd ${⊢}{\phi }\to \left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)\in ℂ$
303 302 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)\in ℂ$
304 fsumconst ${⊢}\left(\left({m}-{s}+1\dots {m}\right)\in \mathrm{Fin}\wedge \left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)\in ℂ\right)\to \sum _{{j}={m}-{s}+1}^{{m}}\left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)=\left|\left({m}-{s}+1\dots {m}\right)\right|\left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)$
305 88 303 304 syl2anc ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}={m}-{s}+1}^{{m}}\left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)=\left|\left({m}-{s}+1\dots {m}\right)\right|\left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)$
306 1zzd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to 1\in ℤ$
307 62 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {s}\in ℤ$
308 fzen ${⊢}\left(1\in ℤ\wedge {s}\in ℤ\wedge {m}-{s}\in ℤ\right)\to \left(1\dots {s}\right)\approx \left(1+{m}-{s}\dots {s}+{m}-{s}\right)$
309 306 307 75 308 syl3anc ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(1\dots {s}\right)\approx \left(1+{m}-{s}\dots {s}+{m}-{s}\right)$
310 ax-1cn ${⊢}1\in ℂ$
311 75 zcnd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}-{s}\in ℂ$
312 addcom ${⊢}\left(1\in ℂ\wedge {m}-{s}\in ℂ\right)\to 1+{m}-{s}={m}-{s}+1$
313 310 311 312 sylancr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to 1+{m}-{s}={m}-{s}+1$
314 262 261 pncan3d ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {s}+{m}-{s}={m}$
315 313 314 oveq12d ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(1+{m}-{s}\dots {s}+{m}-{s}\right)=\left({m}-{s}+1\dots {m}\right)$
316 309 315 breqtrd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(1\dots {s}\right)\approx \left({m}-{s}+1\dots {m}\right)$
317 fzfid ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(1\dots {s}\right)\in \mathrm{Fin}$
318 hashen ${⊢}\left(\left(1\dots {s}\right)\in \mathrm{Fin}\wedge \left({m}-{s}+1\dots {m}\right)\in \mathrm{Fin}\right)\to \left(\left|\left(1\dots {s}\right)\right|=\left|\left({m}-{s}+1\dots {m}\right)\right|↔\left(1\dots {s}\right)\approx \left({m}-{s}+1\dots {m}\right)\right)$
319 317 88 318 syl2anc ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(\left|\left(1\dots {s}\right)\right|=\left|\left({m}-{s}+1\dots {m}\right)\right|↔\left(1\dots {s}\right)\approx \left({m}-{s}+1\dots {m}\right)\right)$
320 316 319 mpbird ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left|\left(1\dots {s}\right)\right|=\left|\left({m}-{s}+1\dots {m}\right)\right|$
321 hashfz1 ${⊢}{s}\in {ℕ}_{0}\to \left|\left(1\dots {s}\right)\right|={s}$
322 53 321 syl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left|\left(1\dots {s}\right)\right|={s}$
323 320 322 eqtr3d ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left|\left({m}-{s}+1\dots {m}\right)\right|={s}$
324 323 oveq1d ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left|\left({m}-{s}+1\dots {m}\right)\right|\left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)={s}\left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)$
325 215 recnd ${⊢}{\phi }\to sup\left({T},ℝ,<\right)\in ℂ$
326 218 rpcnne0d ${⊢}{\phi }\to \left(sup\left({T},ℝ,<\right)+1\in ℂ\wedge sup\left({T},ℝ,<\right)+1\ne 0\right)$
327 div23 ${⊢}\left(\frac{{E}}{2}\in ℂ\wedge sup\left({T},ℝ,<\right)\in ℂ\wedge \left(sup\left({T},ℝ,<\right)+1\in ℂ\wedge sup\left({T},ℝ,<\right)+1\ne 0\right)\right)\to \frac{\left(\frac{{E}}{2}\right)sup\left({T},ℝ,<\right)}{sup\left({T},ℝ,<\right)+1}=\left(\frac{\frac{{E}}{2}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)$
328 160 325 326 327 syl3anc ${⊢}{\phi }\to \frac{\left(\frac{{E}}{2}\right)sup\left({T},ℝ,<\right)}{sup\left({T},ℝ,<\right)+1}=\left(\frac{\frac{{E}}{2}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)$
329 62 zcnd ${⊢}{\phi }\to {s}\in ℂ$
330 222 rpcnd ${⊢}{\phi }\to \frac{\frac{{E}}{2}}{{s}}\in ℂ$
331 divass ${⊢}\left({s}\in ℂ\wedge \frac{\frac{{E}}{2}}{{s}}\in ℂ\wedge \left(sup\left({T},ℝ,<\right)+1\in ℂ\wedge sup\left({T},ℝ,<\right)+1\ne 0\right)\right)\to \frac{{s}\left(\frac{\frac{{E}}{2}}{{s}}\right)}{sup\left({T},ℝ,<\right)+1}={s}\left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)$
332 329 330 326 331 syl3anc ${⊢}{\phi }\to \frac{{s}\left(\frac{\frac{{E}}{2}}{{s}}\right)}{sup\left({T},ℝ,<\right)+1}={s}\left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)$
333 16 nnne0d ${⊢}{\phi }\to {s}\ne 0$
334 160 329 333 divcan2d ${⊢}{\phi }\to {s}\left(\frac{\frac{{E}}{2}}{{s}}\right)=\frac{{E}}{2}$
335 334 oveq1d ${⊢}{\phi }\to \frac{{s}\left(\frac{\frac{{E}}{2}}{{s}}\right)}{sup\left({T},ℝ,<\right)+1}=\frac{\frac{{E}}{2}}{sup\left({T},ℝ,<\right)+1}$
336 332 335 eqtr3d ${⊢}{\phi }\to {s}\left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)=\frac{\frac{{E}}{2}}{sup\left({T},ℝ,<\right)+1}$
337 336 oveq1d ${⊢}{\phi }\to {s}\left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)=\left(\frac{\frac{{E}}{2}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)$
338 223 rpcnd ${⊢}{\phi }\to \frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\in ℂ$
339 329 338 325 mulassd ${⊢}{\phi }\to {s}\left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)={s}\left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)$
340 328 337 339 3eqtr2rd ${⊢}{\phi }\to {s}\left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)=\frac{\left(\frac{{E}}{2}\right)sup\left({T},ℝ,<\right)}{sup\left({T},ℝ,<\right)+1}$
341 340 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {s}\left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)=\frac{\left(\frac{{E}}{2}\right)sup\left({T},ℝ,<\right)}{sup\left({T},ℝ,<\right)+1}$
342 305 324 341 3eqtrd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}={m}-{s}+1}^{{m}}\left(\frac{\frac{\frac{{E}}{2}}{{s}}}{sup\left({T},ℝ,<\right)+1}\right)sup\left({T},ℝ,<\right)=\frac{\left(\frac{{E}}{2}\right)sup\left({T},ℝ,<\right)}{sup\left({T},ℝ,<\right)+1}$
343 301 342 breqtrd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}={m}-{s}+1}^{{m}}\left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\le \frac{\left(\frac{{E}}{2}\right)sup\left({T},ℝ,<\right)}{sup\left({T},ℝ,<\right)+1}$
344 peano2re ${⊢}sup\left({T},ℝ,<\right)\in ℝ\to sup\left({T},ℝ,<\right)+1\in ℝ$
345 215 344 syl ${⊢}{\phi }\to sup\left({T},ℝ,<\right)+1\in ℝ$
346 215 ltp1d ${⊢}{\phi }\to sup\left({T},ℝ,<\right)
347 215 345 99 346 ltmul2dd ${⊢}{\phi }\to \left(\frac{{E}}{2}\right)sup\left({T},ℝ,<\right)<\left(\frac{{E}}{2}\right)\left(sup\left({T},ℝ,<\right)+1\right)$
348 216 100 218 ltdivmul2d ${⊢}{\phi }\to \left(\frac{\left(\frac{{E}}{2}\right)sup\left({T},ℝ,<\right)}{sup\left({T},ℝ,<\right)+1}<\frac{{E}}{2}↔\left(\frac{{E}}{2}\right)sup\left({T},ℝ,<\right)<\left(\frac{{E}}{2}\right)\left(sup\left({T},ℝ,<\right)+1\right)\right)$
349 347 348 mpbird ${⊢}{\phi }\to \frac{\left(\frac{{E}}{2}\right)sup\left({T},ℝ,<\right)}{sup\left({T},ℝ,<\right)+1}<\frac{{E}}{2}$
350 349 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \frac{\left(\frac{{E}}{2}\right)sup\left({T},ℝ,<\right)}{sup\left({T},ℝ,<\right)+1}<\frac{{E}}{2}$
351 98 220 101 343 350 lelttrd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}={m}-{s}+1}^{{m}}\left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|<\frac{{E}}{2}$
352 87 98 101 101 212 351 lt2addd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|+\sum _{{j}={m}-{s}+1}^{{m}}\left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|<\left(\frac{{E}}{2}\right)+\left(\frac{{E}}{2}\right)$
353 24 43 absmuld ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\to \left|{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|=\left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|$
354 353 sumeq2dv ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}}\left|{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|=\sum _{{j}=0}^{{m}}\left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|$
355 75 zred ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}-{s}\in ℝ$
356 355 ltp1d ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {m}-{s}<{m}-{s}+1$
357 fzdisj ${⊢}{m}-{s}<{m}-{s}+1\to \left(0\dots {m}-{s}\right)\cap \left({m}-{s}+1\dots {m}\right)=\varnothing$
358 356 357 syl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(0\dots {m}-{s}\right)\cap \left({m}-{s}+1\dots {m}\right)=\varnothing$
359 fzsplit ${⊢}{m}-{s}\in \left(0\dots {m}\right)\to \left(0\dots {m}\right)=\left(0\dots {m}-{s}\right)\cup \left({m}-{s}+1\dots {m}\right)$
360 73 359 syl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(0\dots {m}\right)=\left(0\dots {m}-{s}\right)\cup \left({m}-{s}+1\dots {m}\right)$
361 85 recnd ${⊢}\left(\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\wedge {j}\in \left(0\dots {m}\right)\right)\to \left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|\in ℂ$
362 358 360 21 361 fsumsplit ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}}\left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|=\sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|+\sum _{{j}={m}-{s}+1}^{{m}}\left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|$
363 354 362 eqtr2d ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}-{s}}\left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|+\sum _{{j}={m}-{s}+1}^{{m}}\left|{A}\right|\left|\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|=\sum _{{j}=0}^{{m}}\left|{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|$
364 9 rpcnd ${⊢}{\phi }\to {E}\in ℂ$
365 364 adantr ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to {E}\in ℂ$
366 365 2halvesd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left(\frac{{E}}{2}\right)+\left(\frac{{E}}{2}\right)={E}$
367 352 363 366 3brtr3d ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \sum _{{j}=0}^{{m}}\left|{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|<{E}$
368 46 48 50 51 367 lelttrd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\right)\to \left|\sum _{{j}=0}^{{m}}{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|<{E}$
369 368 ralrimiva ${⊢}{\phi }\to \forall {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\phantom{\rule{.4em}{0ex}}\left|\sum _{{j}=0}^{{m}}{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|<{E}$
370 fveq2 ${⊢}{y}={s}+{t}\to {ℤ}_{\ge {y}}={ℤ}_{\ge \left({s}+{t}\right)}$
371 370 raleqdv ${⊢}{y}={s}+{t}\to \left(\forall {m}\in {ℤ}_{\ge {y}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{j}=0}^{{m}}{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|<{E}↔\forall {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\phantom{\rule{.4em}{0ex}}\left|\sum _{{j}=0}^{{m}}{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|<{E}\right)$
372 371 rspcev ${⊢}\left({s}+{t}\in {ℕ}_{0}\wedge \forall {m}\in {ℤ}_{\ge \left({s}+{t}\right)}\phantom{\rule{.4em}{0ex}}\left|\sum _{{j}=0}^{{m}}{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|<{E}\right)\to \exists {y}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {y}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{j}=0}^{{m}}{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|<{E}$
373 20 369 372 syl2anc ${⊢}{\phi }\to \exists {y}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {y}}\phantom{\rule{.4em}{0ex}}\left|\sum _{{j}=0}^{{m}}{A}\sum _{{k}\in {ℤ}_{\ge \left({m}-{j}+1\right)}}{B}\right|<{E}$