Metamath Proof Explorer

Theorem mtestbdd

Description: Given the hypotheses of the Weierstrass M-test, the convergent function of the sequence is uniformly bounded. (Contributed by Mario Carneiro, 9-Jul-2017)

Ref Expression
Hypotheses mtest.z ${⊢}{Z}={ℤ}_{\ge {N}}$
mtest.n ${⊢}{\phi }\to {N}\in ℤ$
mtest.s ${⊢}{\phi }\to {S}\in {V}$
mtest.f ${⊢}{\phi }\to {F}:{Z}⟶{ℂ}^{{S}}$
mtest.m ${⊢}{\phi }\to {M}\in {W}$
mtest.c ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {M}\left({k}\right)\in ℝ$
mtest.l ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge {z}\in {S}\right)\right)\to \left|{F}\left({k}\right)\left({z}\right)\right|\le {M}\left({k}\right)$
mtest.d ${⊢}{\phi }\to seq{N}\left(+,{M}\right)\in \mathrm{dom}⇝$
mtest.t
Assertion mtestbdd ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{T}\left({z}\right)\right|\le {x}$

Proof

Step Hyp Ref Expression
1 mtest.z ${⊢}{Z}={ℤ}_{\ge {N}}$
2 mtest.n ${⊢}{\phi }\to {N}\in ℤ$
3 mtest.s ${⊢}{\phi }\to {S}\in {V}$
4 mtest.f ${⊢}{\phi }\to {F}:{Z}⟶{ℂ}^{{S}}$
5 mtest.m ${⊢}{\phi }\to {M}\in {W}$
6 mtest.c ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {M}\left({k}\right)\in ℝ$
7 mtest.l ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge {z}\in {S}\right)\right)\to \left|{F}\left({k}\right)\left({z}\right)\right|\le {M}\left({k}\right)$
8 mtest.d ${⊢}{\phi }\to seq{N}\left(+,{M}\right)\in \mathrm{dom}⇝$
9 mtest.t
10 6 recnd ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {M}\left({k}\right)\in ℂ$
11 1 2 10 serf ${⊢}{\phi }\to seq{N}\left(+,{M}\right):{Z}⟶ℂ$
12 11 ffvelrnda ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to seq{N}\left(+,{M}\right)\left({m}\right)\in ℂ$
13 12 ralrimiva ${⊢}{\phi }\to \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}seq{N}\left(+,{M}\right)\left({m}\right)\in ℂ$
14 1 climbdd ${⊢}\left({N}\in ℤ\wedge seq{N}\left(+,{M}\right)\in \mathrm{dom}⇝\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}seq{N}\left(+,{M}\right)\left({m}\right)\in ℂ\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}$
15 2 8 13 14 syl3anc ${⊢}{\phi }\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}$
16 2 adantr ${⊢}\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\to {N}\in ℤ$
17 seqfn ${⊢}{N}\in ℤ\to seq{N}\left({\circ }_{f}+,{F}\right)Fn{ℤ}_{\ge {N}}$
18 2 17 syl ${⊢}{\phi }\to seq{N}\left({\circ }_{f}+,{F}\right)Fn{ℤ}_{\ge {N}}$
19 1 fneq2i ${⊢}seq{N}\left({\circ }_{f}+,{F}\right)Fn{Z}↔seq{N}\left({\circ }_{f}+,{F}\right)Fn{ℤ}_{\ge {N}}$
20 18 19 sylibr ${⊢}{\phi }\to seq{N}\left({\circ }_{f}+,{F}\right)Fn{Z}$
21 ulmf2
22 20 9 21 syl2anc ${⊢}{\phi }\to seq{N}\left({\circ }_{f}+,{F}\right):{Z}⟶{ℂ}^{{S}}$
23 22 adantr ${⊢}\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\to seq{N}\left({\circ }_{f}+,{F}\right):{Z}⟶{ℂ}^{{S}}$
24 simplrl ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\to {y}\in ℝ$
25 fveq2 ${⊢}{x}={z}\to {F}\left({j}\right)\left({x}\right)={F}\left({j}\right)\left({z}\right)$
26 25 mpteq2dv ${⊢}{x}={z}\to \left({j}\in {Z}⟼{F}\left({j}\right)\left({x}\right)\right)=\left({j}\in {Z}⟼{F}\left({j}\right)\left({z}\right)\right)$
27 26 seqeq3d ${⊢}{x}={z}\to seq{N}\left(+,\left({j}\in {Z}⟼{F}\left({j}\right)\left({x}\right)\right)\right)=seq{N}\left(+,\left({j}\in {Z}⟼{F}\left({j}\right)\left({z}\right)\right)\right)$
28 27 fveq1d ${⊢}{x}={z}\to seq{N}\left(+,\left({j}\in {Z}⟼{F}\left({j}\right)\left({x}\right)\right)\right)\left({n}\right)=seq{N}\left(+,\left({j}\in {Z}⟼{F}\left({j}\right)\left({z}\right)\right)\right)\left({n}\right)$
29 eqid ${⊢}\left({x}\in {S}⟼seq{N}\left(+,\left({j}\in {Z}⟼{F}\left({j}\right)\left({x}\right)\right)\right)\left({n}\right)\right)=\left({x}\in {S}⟼seq{N}\left(+,\left({j}\in {Z}⟼{F}\left({j}\right)\left({x}\right)\right)\right)\left({n}\right)\right)$
30 fvex ${⊢}seq{N}\left(+,\left({j}\in {Z}⟼{F}\left({j}\right)\left({z}\right)\right)\right)\left({n}\right)\in \mathrm{V}$
31 28 29 30 fvmpt ${⊢}{z}\in {S}\to \left({x}\in {S}⟼seq{N}\left(+,\left({j}\in {Z}⟼{F}\left({j}\right)\left({x}\right)\right)\right)\left({n}\right)\right)\left({z}\right)=seq{N}\left(+,\left({j}\in {Z}⟼{F}\left({j}\right)\left({z}\right)\right)\right)\left({n}\right)$
32 31 adantl ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \left({x}\in {S}⟼seq{N}\left(+,\left({j}\in {Z}⟼{F}\left({j}\right)\left({x}\right)\right)\right)\left({n}\right)\right)\left({z}\right)=seq{N}\left(+,\left({j}\in {Z}⟼{F}\left({j}\right)\left({z}\right)\right)\right)\left({n}\right)$
33 4 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to {F}:{Z}⟶{ℂ}^{{S}}$
34 33 feqmptd ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to {F}=\left({j}\in {Z}⟼{F}\left({j}\right)\right)$
35 33 ffvelrnda ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {j}\in {Z}\right)\to {F}\left({j}\right)\in \left({ℂ}^{{S}}\right)$
36 elmapi ${⊢}{F}\left({j}\right)\in \left({ℂ}^{{S}}\right)\to {F}\left({j}\right):{S}⟶ℂ$
37 35 36 syl ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {j}\in {Z}\right)\to {F}\left({j}\right):{S}⟶ℂ$
38 37 feqmptd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {j}\in {Z}\right)\to {F}\left({j}\right)=\left({x}\in {S}⟼{F}\left({j}\right)\left({x}\right)\right)$
39 38 mpteq2dva ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \left({j}\in {Z}⟼{F}\left({j}\right)\right)=\left({j}\in {Z}⟼\left({x}\in {S}⟼{F}\left({j}\right)\left({x}\right)\right)\right)$
40 34 39 eqtrd ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to {F}=\left({j}\in {Z}⟼\left({x}\in {S}⟼{F}\left({j}\right)\left({x}\right)\right)\right)$
41 40 seqeq3d ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to seq{N}\left({\circ }_{f}+,{F}\right)=seq{N}\left({\circ }_{f}+,\left({j}\in {Z}⟼\left({x}\in {S}⟼{F}\left({j}\right)\left({x}\right)\right)\right)\right)$
42 41 fveq1d ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to seq{N}\left({\circ }_{f}+,{F}\right)\left({n}\right)=seq{N}\left({\circ }_{f}+,\left({j}\in {Z}⟼\left({x}\in {S}⟼{F}\left({j}\right)\left({x}\right)\right)\right)\right)\left({n}\right)$
43 3 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to {S}\in {V}$
44 simplr ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to {n}\in {Z}$
45 44 1 syl6eleq ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to {n}\in {ℤ}_{\ge {N}}$
46 elfzuz ${⊢}{k}\in \left({N}\dots {n}\right)\to {k}\in {ℤ}_{\ge {N}}$
47 46 1 syl6eleqr ${⊢}{k}\in \left({N}\dots {n}\right)\to {k}\in {Z}$
48 47 ssriv ${⊢}\left({N}\dots {n}\right)\subseteq {Z}$
49 48 a1i ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \left({N}\dots {n}\right)\subseteq {Z}$
50 37 ffvelrnda ${⊢}\left(\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {j}\in {Z}\right)\wedge {x}\in {S}\right)\to {F}\left({j}\right)\left({x}\right)\in ℂ$
51 50 anasss ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge \left({j}\in {Z}\wedge {x}\in {S}\right)\right)\to {F}\left({j}\right)\left({x}\right)\in ℂ$
52 43 45 49 51 seqof2 ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to seq{N}\left({\circ }_{f}+,\left({j}\in {Z}⟼\left({x}\in {S}⟼{F}\left({j}\right)\left({x}\right)\right)\right)\right)\left({n}\right)=\left({x}\in {S}⟼seq{N}\left(+,\left({j}\in {Z}⟼{F}\left({j}\right)\left({x}\right)\right)\right)\left({n}\right)\right)$
53 42 52 eqtrd ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to seq{N}\left({\circ }_{f}+,{F}\right)\left({n}\right)=\left({x}\in {S}⟼seq{N}\left(+,\left({j}\in {Z}⟼{F}\left({j}\right)\left({x}\right)\right)\right)\left({n}\right)\right)$
54 53 fveq1d ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to seq{N}\left({\circ }_{f}+,{F}\right)\left({n}\right)\left({z}\right)=\left({x}\in {S}⟼seq{N}\left(+,\left({j}\in {Z}⟼{F}\left({j}\right)\left({x}\right)\right)\right)\left({n}\right)\right)\left({z}\right)$
55 47 adantl ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {k}\in \left({N}\dots {n}\right)\right)\to {k}\in {Z}$
56 fveq2 ${⊢}{j}={k}\to {F}\left({j}\right)={F}\left({k}\right)$
57 56 fveq1d ${⊢}{j}={k}\to {F}\left({j}\right)\left({z}\right)={F}\left({k}\right)\left({z}\right)$
58 eqid ${⊢}\left({j}\in {Z}⟼{F}\left({j}\right)\left({z}\right)\right)=\left({j}\in {Z}⟼{F}\left({j}\right)\left({z}\right)\right)$
59 fvex ${⊢}{F}\left({k}\right)\left({z}\right)\in \mathrm{V}$
60 57 58 59 fvmpt ${⊢}{k}\in {Z}\to \left({j}\in {Z}⟼{F}\left({j}\right)\left({z}\right)\right)\left({k}\right)={F}\left({k}\right)\left({z}\right)$
61 55 60 syl ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {k}\in \left({N}\dots {n}\right)\right)\to \left({j}\in {Z}⟼{F}\left({j}\right)\left({z}\right)\right)\left({k}\right)={F}\left({k}\right)\left({z}\right)$
62 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {j}\in {Z}\right)\to {z}\in {S}$
63 37 62 ffvelrnd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {j}\in {Z}\right)\to {F}\left({j}\right)\left({z}\right)\in ℂ$
64 63 fmpttd ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \left({j}\in {Z}⟼{F}\left({j}\right)\left({z}\right)\right):{Z}⟶ℂ$
65 64 ffvelrnda ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {k}\in {Z}\right)\to \left({j}\in {Z}⟼{F}\left({j}\right)\left({z}\right)\right)\left({k}\right)\in ℂ$
66 47 65 sylan2 ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {k}\in \left({N}\dots {n}\right)\right)\to \left({j}\in {Z}⟼{F}\left({j}\right)\left({z}\right)\right)\left({k}\right)\in ℂ$
67 61 66 eqeltrrd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {k}\in \left({N}\dots {n}\right)\right)\to {F}\left({k}\right)\left({z}\right)\in ℂ$
68 61 45 67 fsumser ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \sum _{{k}={N}}^{{n}}{F}\left({k}\right)\left({z}\right)=seq{N}\left(+,\left({j}\in {Z}⟼{F}\left({j}\right)\left({z}\right)\right)\right)\left({n}\right)$
69 32 54 68 3eqtr4d ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to seq{N}\left({\circ }_{f}+,{F}\right)\left({n}\right)\left({z}\right)=\sum _{{k}={N}}^{{n}}{F}\left({k}\right)\left({z}\right)$
70 69 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \left|seq{N}\left({\circ }_{f}+,{F}\right)\left({n}\right)\left({z}\right)\right|=\left|\sum _{{k}={N}}^{{n}}{F}\left({k}\right)\left({z}\right)\right|$
71 fzfid ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \left({N}\dots {n}\right)\in \mathrm{Fin}$
72 71 67 fsumcl ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \sum _{{k}={N}}^{{n}}{F}\left({k}\right)\left({z}\right)\in ℂ$
73 72 abscld ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \left|\sum _{{k}={N}}^{{n}}{F}\left({k}\right)\left({z}\right)\right|\in ℝ$
74 67 abscld ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {k}\in \left({N}\dots {n}\right)\right)\to \left|{F}\left({k}\right)\left({z}\right)\right|\in ℝ$
75 71 74 fsumrecl ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \sum _{{k}={N}}^{{n}}\left|{F}\left({k}\right)\left({z}\right)\right|\in ℝ$
76 24 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to {y}\in ℝ$
77 71 67 fsumabs ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \left|\sum _{{k}={N}}^{{n}}{F}\left({k}\right)\left({z}\right)\right|\le \sum _{{k}={N}}^{{n}}\left|{F}\left({k}\right)\left({z}\right)\right|$
78 simp-4l ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {k}\in \left({N}\dots {n}\right)\right)\to {\phi }$
79 78 55 6 syl2anc ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {k}\in \left({N}\dots {n}\right)\right)\to {M}\left({k}\right)\in ℝ$
80 71 79 fsumrecl ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \sum _{{k}={N}}^{{n}}{M}\left({k}\right)\in ℝ$
81 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {k}\in \left({N}\dots {n}\right)\right)\to {z}\in {S}$
82 78 55 81 7 syl12anc ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {k}\in \left({N}\dots {n}\right)\right)\to \left|{F}\left({k}\right)\left({z}\right)\right|\le {M}\left({k}\right)$
83 71 74 79 82 fsumle ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \sum _{{k}={N}}^{{n}}\left|{F}\left({k}\right)\left({z}\right)\right|\le \sum _{{k}={N}}^{{n}}{M}\left({k}\right)$
84 80 recnd ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \sum _{{k}={N}}^{{n}}{M}\left({k}\right)\in ℂ$
85 84 abscld ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \left|\sum _{{k}={N}}^{{n}}{M}\left({k}\right)\right|\in ℝ$
86 80 leabsd ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \sum _{{k}={N}}^{{n}}{M}\left({k}\right)\le \left|\sum _{{k}={N}}^{{n}}{M}\left({k}\right)\right|$
87 eqidd ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {k}\in \left({N}\dots {n}\right)\right)\to {M}\left({k}\right)={M}\left({k}\right)$
88 78 55 10 syl2anc ${⊢}\left(\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\wedge {k}\in \left({N}\dots {n}\right)\right)\to {M}\left({k}\right)\in ℂ$
89 87 45 88 fsumser ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \sum _{{k}={N}}^{{n}}{M}\left({k}\right)=seq{N}\left(+,{M}\right)\left({n}\right)$
90 89 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \left|\sum _{{k}={N}}^{{n}}{M}\left({k}\right)\right|=\left|seq{N}\left(+,{M}\right)\left({n}\right)\right|$
91 simprr ${⊢}\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\to \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}$
92 fveq2 ${⊢}{m}={n}\to seq{N}\left(+,{M}\right)\left({m}\right)=seq{N}\left(+,{M}\right)\left({n}\right)$
93 92 fveq2d ${⊢}{m}={n}\to \left|seq{N}\left(+,{M}\right)\left({m}\right)\right|=\left|seq{N}\left(+,{M}\right)\left({n}\right)\right|$
94 93 breq1d ${⊢}{m}={n}\to \left(\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}↔\left|seq{N}\left(+,{M}\right)\left({n}\right)\right|\le {y}\right)$
95 94 rspccva ${⊢}\left(\forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\wedge {n}\in {Z}\right)\to \left|seq{N}\left(+,{M}\right)\left({n}\right)\right|\le {y}$
96 91 95 sylan ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\to \left|seq{N}\left(+,{M}\right)\left({n}\right)\right|\le {y}$
97 96 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \left|seq{N}\left(+,{M}\right)\left({n}\right)\right|\le {y}$
98 90 97 eqbrtrd ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \left|\sum _{{k}={N}}^{{n}}{M}\left({k}\right)\right|\le {y}$
99 80 85 76 86 98 letrd ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \sum _{{k}={N}}^{{n}}{M}\left({k}\right)\le {y}$
100 75 80 76 83 99 letrd ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \sum _{{k}={N}}^{{n}}\left|{F}\left({k}\right)\left({z}\right)\right|\le {y}$
101 73 75 76 77 100 letrd ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \left|\sum _{{k}={N}}^{{n}}{F}\left({k}\right)\left({z}\right)\right|\le {y}$
102 70 101 eqbrtrd ${⊢}\left(\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\wedge {z}\in {S}\right)\to \left|seq{N}\left({\circ }_{f}+,{F}\right)\left({n}\right)\left({z}\right)\right|\le {y}$
103 102 ralrimiva ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\to \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left({\circ }_{f}+,{F}\right)\left({n}\right)\left({z}\right)\right|\le {y}$
104 brralrspcev ${⊢}\left({y}\in ℝ\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left({\circ }_{f}+,{F}\right)\left({n}\right)\left({z}\right)\right|\le {y}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left({\circ }_{f}+,{F}\right)\left({n}\right)\left({z}\right)\right|\le {x}$
105 24 103 104 syl2anc ${⊢}\left(\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\wedge {n}\in {Z}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left({\circ }_{f}+,{F}\right)\left({n}\right)\left({z}\right)\right|\le {x}$
107 1 16 23 105 106 ulmbdd ${⊢}\left({\phi }\wedge \left({y}\in ℝ\wedge \forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}\left|seq{N}\left(+,{M}\right)\left({m}\right)\right|\le {y}\right)\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{T}\left({z}\right)\right|\le {x}$
108 15 107 rexlimddv ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left|{T}\left({z}\right)\right|\le {x}$