# Metamath Proof Explorer

## Theorem fourierdlem87

Description: The integral of G goes uniformly ( with respect to n ) to zero if the measure of the domain of integration goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem87.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
fourierdlem87.x ${⊢}{\phi }\to {X}\in ℝ$
fourierdlem87.y ${⊢}{\phi }\to {Y}\in ℝ$
fourierdlem87.w ${⊢}{\phi }\to {W}\in ℝ$
fourierdlem87.h ${⊢}{H}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({s}=0,0,\frac{{F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)}{{s}}\right)\right)$
fourierdlem87.k ${⊢}{K}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({s}=0,1,\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)$
fourierdlem87.u ${⊢}{U}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{H}\left({s}\right){K}\left({s}\right)\right)$
fourierdlem87.s ${⊢}{S}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right)$
fourierdlem87.g ${⊢}{G}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{U}\left({s}\right){S}\left({s}\right)\right)$
fourierdlem87.10 ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{H}\left({s}\right)\right|\le {x}$
fourierdlem87.gibl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {G}\in {𝐿}^{1}$
fourierdlem87.d ${⊢}{D}=\frac{\frac{{e}}{3}}{{a}}$
fourierdlem87.ch ${⊢}{\chi }↔\left(\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\wedge \left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\right)\wedge {n}\in ℕ\right)$
Assertion fourierdlem87 ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {d}\right)\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{e}}{2}\right)$

### Proof

Step Hyp Ref Expression
1 fourierdlem87.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
2 fourierdlem87.x ${⊢}{\phi }\to {X}\in ℝ$
3 fourierdlem87.y ${⊢}{\phi }\to {Y}\in ℝ$
4 fourierdlem87.w ${⊢}{\phi }\to {W}\in ℝ$
5 fourierdlem87.h ${⊢}{H}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({s}=0,0,\frac{{F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)}{{s}}\right)\right)$
6 fourierdlem87.k ${⊢}{K}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({s}=0,1,\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)$
7 fourierdlem87.u ${⊢}{U}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{H}\left({s}\right){K}\left({s}\right)\right)$
8 fourierdlem87.s ${⊢}{S}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right)$
9 fourierdlem87.g ${⊢}{G}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{U}\left({s}\right){S}\left({s}\right)\right)$
10 fourierdlem87.10 ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{H}\left({s}\right)\right|\le {x}$
11 fourierdlem87.gibl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {G}\in {𝐿}^{1}$
12 fourierdlem87.d ${⊢}{D}=\frac{\frac{{e}}{3}}{{a}}$
13 fourierdlem87.ch ${⊢}{\chi }↔\left(\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\wedge \left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\right)\wedge {n}\in ℕ\right)$
14 1 2 3 4 5 6 7 10 fourierdlem77 ${⊢}{\phi }\to \exists {a}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}$
15 nfv ${⊢}Ⅎ{s}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {a}\in {ℝ}^{+}\right)$
16 nfra1 ${⊢}Ⅎ{s}\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}$
17 15 16 nfan ${⊢}Ⅎ{s}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}\right)$
18 nfv ${⊢}Ⅎ{s}\phantom{\rule{.4em}{0ex}}{n}\in ℕ$
19 17 18 nfan ${⊢}Ⅎ{s}\phantom{\rule{.4em}{0ex}}\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}\right)\wedge {n}\in ℕ\right)$
20 simp-4l ${⊢}\left(\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {\phi }$
21 simp-4r ${⊢}\left(\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {a}\in {ℝ}^{+}$
22 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {n}\in ℕ$
23 20 21 22 jca31 ${⊢}\left(\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge {n}\in ℕ\right)$
24 simpr ${⊢}\left(\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]$
25 simpllr ${⊢}\left(\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}$
26 rspa ${⊢}\left(\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|{U}\left({s}\right)\right|\le {a}$
27 25 24 26 syl2anc ${⊢}\left(\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|{U}\left({s}\right)\right|\le {a}$
28 simpr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]$
29 1 2 3 4 5 6 7 fourierdlem55 ${⊢}{\phi }\to {U}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
30 29 ffvelrnda ${⊢}\left({\phi }\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {U}\left({s}\right)\in ℝ$
31 30 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {U}\left({s}\right)\in ℝ$
32 nnre ${⊢}{n}\in ℕ\to {n}\in ℝ$
33 8 fourierdlem5 ${⊢}{n}\in ℝ\to {S}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
34 32 33 syl ${⊢}{n}\in ℕ\to {S}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
35 34 ad2antlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {S}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
36 35 28 ffvelrnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {S}\left({s}\right)\in ℝ$
37 31 36 remulcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {U}\left({s}\right){S}\left({s}\right)\in ℝ$
38 9 fvmpt2 ${⊢}\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge {U}\left({s}\right){S}\left({s}\right)\in ℝ\right)\to {G}\left({s}\right)={U}\left({s}\right){S}\left({s}\right)$
39 28 37 38 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {G}\left({s}\right)={U}\left({s}\right){S}\left({s}\right)$
40 simpr ${⊢}\left({n}\in ℕ\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]$
41 halfre ${⊢}\frac{1}{2}\in ℝ$
42 41 a1i ${⊢}{n}\in ℕ\to \frac{1}{2}\in ℝ$
43 32 42 readdcld ${⊢}{n}\in ℕ\to {n}+\left(\frac{1}{2}\right)\in ℝ$
44 43 adantr ${⊢}\left({n}\in ℕ\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {n}+\left(\frac{1}{2}\right)\in ℝ$
45 pire ${⊢}\mathrm{\pi }\in ℝ$
46 45 renegcli ${⊢}-\mathrm{\pi }\in ℝ$
47 iccssre ${⊢}\left(-\mathrm{\pi }\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \left[-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℝ$
48 46 45 47 mp2an ${⊢}\left[-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℝ$
49 48 sseli ${⊢}{s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\to {s}\in ℝ$
50 49 adantl ${⊢}\left({n}\in ℕ\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {s}\in ℝ$
51 44 50 remulcld ${⊢}\left({n}\in ℕ\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left({n}+\left(\frac{1}{2}\right)\right){s}\in ℝ$
52 51 resincld ${⊢}\left({n}\in ℕ\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\in ℝ$
53 8 fvmpt2 ${⊢}\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge \mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\in ℝ\right)\to {S}\left({s}\right)=\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}$
54 40 52 53 syl2anc ${⊢}\left({n}\in ℕ\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {S}\left({s}\right)=\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}$
55 54 oveq2d ${⊢}\left({n}\in ℕ\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {U}\left({s}\right){S}\left({s}\right)={U}\left({s}\right)\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}$
56 55 adantll ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {U}\left({s}\right){S}\left({s}\right)={U}\left({s}\right)\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}$
57 39 56 eqtrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {G}\left({s}\right)={U}\left({s}\right)\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}$
58 57 fveq2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|{G}\left({s}\right)\right|=\left|{U}\left({s}\right)\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right|$
59 31 recnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {U}\left({s}\right)\in ℂ$
60 52 adantll ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\in ℝ$
61 60 recnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\in ℂ$
62 59 61 absmuld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|{U}\left({s}\right)\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right|=\left|{U}\left({s}\right)\right|\left|\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right|$
63 58 62 eqtrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|{G}\left({s}\right)\right|=\left|{U}\left({s}\right)\right|\left|\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right|$
64 63 adantllr ${⊢}\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|{G}\left({s}\right)\right|=\left|{U}\left({s}\right)\right|\left|\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right|$
65 64 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\wedge \left|{U}\left({s}\right)\right|\le {a}\right)\to \left|{G}\left({s}\right)\right|=\left|{U}\left({s}\right)\right|\left|\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right|$
66 59 abscld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|{U}\left({s}\right)\right|\in ℝ$
67 61 abscld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right|\in ℝ$
68 66 67 remulcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|{U}\left({s}\right)\right|\left|\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right|\in ℝ$
69 68 adantllr ${⊢}\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|{U}\left({s}\right)\right|\left|\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right|\in ℝ$
70 69 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\wedge \left|{U}\left({s}\right)\right|\le {a}\right)\to \left|{U}\left({s}\right)\right|\left|\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right|\in ℝ$
71 66 adantllr ${⊢}\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|{U}\left({s}\right)\right|\in ℝ$
72 71 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\wedge \left|{U}\left({s}\right)\right|\le {a}\right)\to \left|{U}\left({s}\right)\right|\in ℝ$
73 rpre ${⊢}{a}\in {ℝ}^{+}\to {a}\in ℝ$
74 73 ad4antlr ${⊢}\left(\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\wedge \left|{U}\left({s}\right)\right|\le {a}\right)\to {a}\in ℝ$
75 1red ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to 1\in ℝ$
76 59 absge0d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to 0\le \left|{U}\left({s}\right)\right|$
77 51 adantll ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left({n}+\left(\frac{1}{2}\right)\right){s}\in ℝ$
78 abssinbd ${⊢}\left({n}+\left(\frac{1}{2}\right)\right){s}\in ℝ\to \left|\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right|\le 1$
79 77 78 syl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right|\le 1$
80 67 75 66 76 79 lemul2ad ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|{U}\left({s}\right)\right|\left|\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right|\le \left|{U}\left({s}\right)\right|\cdot 1$
81 66 recnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|{U}\left({s}\right)\right|\in ℂ$
82 81 mulid1d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|{U}\left({s}\right)\right|\cdot 1=\left|{U}\left({s}\right)\right|$
83 80 82 breqtrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|{U}\left({s}\right)\right|\left|\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right|\le \left|{U}\left({s}\right)\right|$
84 83 adantllr ${⊢}\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|{U}\left({s}\right)\right|\left|\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right|\le \left|{U}\left({s}\right)\right|$
85 84 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\wedge \left|{U}\left({s}\right)\right|\le {a}\right)\to \left|{U}\left({s}\right)\right|\left|\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right|\le \left|{U}\left({s}\right)\right|$
86 simpr ${⊢}\left(\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\wedge \left|{U}\left({s}\right)\right|\le {a}\right)\to \left|{U}\left({s}\right)\right|\le {a}$
87 70 72 74 85 86 letrd ${⊢}\left(\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\wedge \left|{U}\left({s}\right)\right|\le {a}\right)\to \left|{U}\left({s}\right)\right|\left|\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right|\le {a}$
88 65 87 eqbrtrd ${⊢}\left(\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\wedge \left|{U}\left({s}\right)\right|\le {a}\right)\to \left|{G}\left({s}\right)\right|\le {a}$
89 23 24 27 88 syl21anc ${⊢}\left(\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}\right)\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|{G}\left({s}\right)\right|\le {a}$
90 89 ex ${⊢}\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}\right)\wedge {n}\in ℕ\right)\to \left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\to \left|{G}\left({s}\right)\right|\le {a}\right)$
91 19 90 ralrimi ${⊢}\left(\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}\right)\wedge {n}\in ℕ\right)\to \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}$
92 91 ralrimiva ${⊢}\left(\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\wedge \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}$
93 92 ex ${⊢}\left({\phi }\wedge {a}\in {ℝ}^{+}\right)\to \left(\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)$
94 93 reximdva ${⊢}{\phi }\to \left(\exists {a}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{U}\left({s}\right)\right|\le {a}\to \exists {a}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)$
95 14 94 mpd ${⊢}{\phi }\to \exists {a}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}$
96 95 adantr ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \exists {a}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}$
97 id ${⊢}{e}\in {ℝ}^{+}\to {e}\in {ℝ}^{+}$
98 3rp ${⊢}3\in {ℝ}^{+}$
99 98 a1i ${⊢}{e}\in {ℝ}^{+}\to 3\in {ℝ}^{+}$
100 97 99 rpdivcld ${⊢}{e}\in {ℝ}^{+}\to \frac{{e}}{3}\in {ℝ}^{+}$
101 100 adantr ${⊢}\left({e}\in {ℝ}^{+}\wedge {a}\in {ℝ}^{+}\right)\to \frac{{e}}{3}\in {ℝ}^{+}$
102 simpr ${⊢}\left({e}\in {ℝ}^{+}\wedge {a}\in {ℝ}^{+}\right)\to {a}\in {ℝ}^{+}$
103 101 102 rpdivcld ${⊢}\left({e}\in {ℝ}^{+}\wedge {a}\in {ℝ}^{+}\right)\to \frac{\frac{{e}}{3}}{{a}}\in {ℝ}^{+}$
104 12 103 eqeltrid ${⊢}\left({e}\in {ℝ}^{+}\wedge {a}\in {ℝ}^{+}\right)\to {D}\in {ℝ}^{+}$
105 104 adantll ${⊢}\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\right)\to {D}\in {ℝ}^{+}$
106 105 3adant3 ${⊢}\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\to {D}\in {ℝ}^{+}$
107 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)$
108 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{a}\in {ℝ}^{+}$
109 nfra1 ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}$
110 107 108 109 nf3an ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)$
111 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{u}\in \mathrm{dom}vol$
112 110 111 nfan ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)$
113 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)$
114 112 113 nfan ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\wedge \left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\right)$
115 simpl1l ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\to {\phi }$
116 115 ad2antrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\wedge \left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\right)\wedge {n}\in ℕ\right)\to {\phi }$
117 13 116 sylbi ${⊢}{\chi }\to {\phi }$
118 117 1 syl ${⊢}{\chi }\to {F}:ℝ⟶ℝ$
119 117 2 syl ${⊢}{\chi }\to {X}\in ℝ$
120 117 3 syl ${⊢}{\chi }\to {Y}\in ℝ$
121 117 4 syl ${⊢}{\chi }\to {W}\in ℝ$
122 32 adantl ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\wedge \left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\right)\wedge {n}\in ℕ\right)\to {n}\in ℝ$
123 13 122 sylbi ${⊢}{\chi }\to {n}\in ℝ$
124 118 119 120 121 5 6 7 123 8 9 fourierdlem67 ${⊢}{\chi }\to {G}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
125 124 adantr ${⊢}\left({\chi }\wedge {s}\in {u}\right)\to {G}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
126 simplrl ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\wedge \left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\right)\wedge {n}\in ℕ\right)\to {u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
127 13 126 sylbi ${⊢}{\chi }\to {u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
128 127 sselda ${⊢}\left({\chi }\wedge {s}\in {u}\right)\to {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]$
129 125 128 ffvelrnd ${⊢}\left({\chi }\wedge {s}\in {u}\right)\to {G}\left({s}\right)\in ℝ$
130 simpllr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\wedge \left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\right)\wedge {n}\in ℕ\right)\to {u}\in \mathrm{dom}vol$
131 13 130 sylbi ${⊢}{\chi }\to {u}\in \mathrm{dom}vol$
132 124 ffvelrnda ${⊢}\left({\chi }\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {G}\left({s}\right)\in ℝ$
133 124 feqmptd ${⊢}{\chi }\to {G}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{G}\left({s}\right)\right)$
134 13 simprbi ${⊢}{\chi }\to {n}\in ℕ$
135 117 134 11 syl2anc ${⊢}{\chi }\to {G}\in {𝐿}^{1}$
136 133 135 eqeltrrd ${⊢}{\chi }\to \left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{G}\left({s}\right)\right)\in {𝐿}^{1}$
137 127 131 132 136 iblss ${⊢}{\chi }\to \left({s}\in {u}⟼{G}\left({s}\right)\right)\in {𝐿}^{1}$
138 129 137 itgcl ${⊢}{\chi }\to {\int }_{{u}}{G}\left({s}\right)d{s}\in ℂ$
139 138 abscld ${⊢}{\chi }\to \left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|\in ℝ$
140 129 recnd ${⊢}\left({\chi }\wedge {s}\in {u}\right)\to {G}\left({s}\right)\in ℂ$
141 140 abscld ${⊢}\left({\chi }\wedge {s}\in {u}\right)\to \left|{G}\left({s}\right)\right|\in ℝ$
142 129 137 iblabs ${⊢}{\chi }\to \left({s}\in {u}⟼\left|{G}\left({s}\right)\right|\right)\in {𝐿}^{1}$
143 141 142 itgrecl ${⊢}{\chi }\to {\int }_{{u}}\left|{G}\left({s}\right)\right|d{s}\in ℝ$
144 simpl1r ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\to {e}\in {ℝ}^{+}$
145 144 ad2antrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\wedge \left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\right)\wedge {n}\in ℕ\right)\to {e}\in {ℝ}^{+}$
146 13 145 sylbi ${⊢}{\chi }\to {e}\in {ℝ}^{+}$
147 146 rpred ${⊢}{\chi }\to {e}\in ℝ$
148 147 rehalfcld ${⊢}{\chi }\to \frac{{e}}{2}\in ℝ$
149 129 137 itgabs ${⊢}{\chi }\to \left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|\le {\int }_{{u}}\left|{G}\left({s}\right)\right|d{s}$
150 simpl2 ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\to {a}\in {ℝ}^{+}$
151 150 ad2antrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\wedge \left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\right)\wedge {n}\in ℕ\right)\to {a}\in {ℝ}^{+}$
152 13 151 sylbi ${⊢}{\chi }\to {a}\in {ℝ}^{+}$
153 152 rpred ${⊢}{\chi }\to {a}\in ℝ$
154 153 adantr ${⊢}\left({\chi }\wedge {s}\in {u}\right)\to {a}\in ℝ$
155 iccssxr ${⊢}\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$
156 volf ${⊢}vol:\mathrm{dom}vol⟶\left[0,\mathrm{+\infty }\right]$
157 156 a1i ${⊢}{\chi }\to vol:\mathrm{dom}vol⟶\left[0,\mathrm{+\infty }\right]$
158 157 131 ffvelrnd ${⊢}{\chi }\to vol\left({u}\right)\in \left[0,\mathrm{+\infty }\right]$
159 155 158 sseldi ${⊢}{\chi }\to vol\left({u}\right)\in {ℝ}^{*}$
160 iccvolcl ${⊢}\left(-\mathrm{\pi }\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to vol\left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\in ℝ$
161 46 45 160 mp2an ${⊢}vol\left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\in ℝ$
162 161 a1i ${⊢}{\chi }\to vol\left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\in ℝ$
163 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
164 163 a1i ${⊢}{\chi }\to \mathrm{-\infty }\in {ℝ}^{*}$
165 0xr ${⊢}0\in {ℝ}^{*}$
166 165 a1i ${⊢}{\chi }\to 0\in {ℝ}^{*}$
167 mnflt0 ${⊢}\mathrm{-\infty }<0$
168 167 a1i ${⊢}{\chi }\to \mathrm{-\infty }<0$
169 volge0 ${⊢}{u}\in \mathrm{dom}vol\to 0\le vol\left({u}\right)$
170 131 169 syl ${⊢}{\chi }\to 0\le vol\left({u}\right)$
171 164 166 159 168 170 xrltletrd ${⊢}{\chi }\to \mathrm{-\infty }
172 iccmbl ${⊢}\left(-\mathrm{\pi }\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \left[-\mathrm{\pi },\mathrm{\pi }\right]\in \mathrm{dom}vol$
173 46 45 172 mp2an ${⊢}\left[-\mathrm{\pi },\mathrm{\pi }\right]\in \mathrm{dom}vol$
174 173 a1i ${⊢}{\chi }\to \left[-\mathrm{\pi },\mathrm{\pi }\right]\in \mathrm{dom}vol$
175 volss ${⊢}\left({u}\in \mathrm{dom}vol\wedge \left[-\mathrm{\pi },\mathrm{\pi }\right]\in \mathrm{dom}vol\wedge {u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to vol\left({u}\right)\le vol\left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\right)$
176 131 174 127 175 syl3anc ${⊢}{\chi }\to vol\left({u}\right)\le vol\left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\right)$
177 xrre ${⊢}\left(\left(vol\left({u}\right)\in {ℝ}^{*}\wedge vol\left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\in ℝ\right)\wedge \left(\mathrm{-\infty }
178 159 162 171 176 177 syl22anc ${⊢}{\chi }\to vol\left({u}\right)\in ℝ$
179 152 rpcnd ${⊢}{\chi }\to {a}\in ℂ$
180 iblconstmpt ${⊢}\left({u}\in \mathrm{dom}vol\wedge vol\left({u}\right)\in ℝ\wedge {a}\in ℂ\right)\to \left({s}\in {u}⟼{a}\right)\in {𝐿}^{1}$
181 131 178 179 180 syl3anc ${⊢}{\chi }\to \left({s}\in {u}⟼{a}\right)\in {𝐿}^{1}$
182 154 181 itgrecl ${⊢}{\chi }\to {\int }_{{u}}{a}d{s}\in ℝ$
183 simpl3 ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}$
184 183 ad2antrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\wedge \left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\right)\wedge {n}\in ℕ\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}$
185 13 184 sylbi ${⊢}{\chi }\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}$
186 rspa ${⊢}\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\wedge {n}\in ℕ\right)\to \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}$
187 185 134 186 syl2anc ${⊢}{\chi }\to \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}$
188 187 adantr ${⊢}\left({\chi }\wedge {s}\in {u}\right)\to \forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}$
189 rspa ${⊢}\left(\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left|{G}\left({s}\right)\right|\le {a}$
190 188 128 189 syl2anc ${⊢}\left({\chi }\wedge {s}\in {u}\right)\to \left|{G}\left({s}\right)\right|\le {a}$
191 142 181 141 154 190 itgle ${⊢}{\chi }\to {\int }_{{u}}\left|{G}\left({s}\right)\right|d{s}\le {\int }_{{u}}{a}d{s}$
192 itgconst ${⊢}\left({u}\in \mathrm{dom}vol\wedge vol\left({u}\right)\in ℝ\wedge {a}\in ℂ\right)\to {\int }_{{u}}{a}d{s}={a}vol\left({u}\right)$
193 131 178 179 192 syl3anc ${⊢}{\chi }\to {\int }_{{u}}{a}d{s}={a}vol\left({u}\right)$
194 153 178 remulcld ${⊢}{\chi }\to {a}vol\left({u}\right)\in ℝ$
195 3re ${⊢}3\in ℝ$
196 195 a1i ${⊢}{\chi }\to 3\in ℝ$
197 3ne0 ${⊢}3\ne 0$
198 197 a1i ${⊢}{\chi }\to 3\ne 0$
199 147 196 198 redivcld ${⊢}{\chi }\to \frac{{e}}{3}\in ℝ$
200 152 rpne0d ${⊢}{\chi }\to {a}\ne 0$
201 199 153 200 redivcld ${⊢}{\chi }\to \frac{\frac{{e}}{3}}{{a}}\in ℝ$
202 12 201 eqeltrid ${⊢}{\chi }\to {D}\in ℝ$
203 153 202 remulcld ${⊢}{\chi }\to {a}{D}\in ℝ$
204 152 rpge0d ${⊢}{\chi }\to 0\le {a}$
205 simplrr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\wedge \left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\right)\wedge {n}\in ℕ\right)\to vol\left({u}\right)\le {D}$
206 13 205 sylbi ${⊢}{\chi }\to vol\left({u}\right)\le {D}$
207 178 202 153 204 206 lemul2ad ${⊢}{\chi }\to {a}vol\left({u}\right)\le {a}{D}$
208 12 oveq2i ${⊢}{a}{D}={a}\left(\frac{\frac{{e}}{3}}{{a}}\right)$
209 199 recnd ${⊢}{\chi }\to \frac{{e}}{3}\in ℂ$
210 209 179 200 divcan2d ${⊢}{\chi }\to {a}\left(\frac{\frac{{e}}{3}}{{a}}\right)=\frac{{e}}{3}$
211 208 210 syl5eq ${⊢}{\chi }\to {a}{D}=\frac{{e}}{3}$
212 2rp ${⊢}2\in {ℝ}^{+}$
213 212 a1i ${⊢}{\chi }\to 2\in {ℝ}^{+}$
214 98 a1i ${⊢}{\chi }\to 3\in {ℝ}^{+}$
215 2lt3 ${⊢}2<3$
216 215 a1i ${⊢}{\chi }\to 2<3$
217 213 214 146 216 ltdiv2dd ${⊢}{\chi }\to \frac{{e}}{3}<\frac{{e}}{2}$
218 211 217 eqbrtrd ${⊢}{\chi }\to {a}{D}<\frac{{e}}{2}$
219 194 203 148 207 218 lelttrd ${⊢}{\chi }\to {a}vol\left({u}\right)<\frac{{e}}{2}$
220 193 219 eqbrtrd ${⊢}{\chi }\to {\int }_{{u}}{a}d{s}<\frac{{e}}{2}$
221 143 182 148 191 220 lelttrd ${⊢}{\chi }\to {\int }_{{u}}\left|{G}\left({s}\right)\right|d{s}<\frac{{e}}{2}$
222 139 143 148 149 221 lelttrd ${⊢}{\chi }\to \left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}$
223 13 222 sylbir ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\wedge \left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\right)\wedge {n}\in ℕ\right)\to \left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}$
224 223 ex ${⊢}\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\wedge \left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\right)\to \left({n}\in ℕ\to \left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}\right)$
225 114 224 ralrimi ${⊢}\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\wedge \left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}$
226 225 ex ${⊢}\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\wedge {u}\in \mathrm{dom}vol\right)\to \left(\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}\right)$
227 226 ralrimiva ${⊢}\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\to \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}\right)$
228 breq2 ${⊢}{d}={D}\to \left(vol\left({u}\right)\le {d}↔vol\left({u}\right)\le {D}\right)$
229 228 anbi2d ${⊢}{d}={D}\to \left(\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {d}\right)↔\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\right)$
230 229 rspceaimv ${⊢}\left({D}\in {ℝ}^{+}\wedge \forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {D}\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}\right)\right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {d}\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}\right)$
231 106 227 230 syl2anc ${⊢}\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {a}\in {ℝ}^{+}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {d}\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}\right)$
232 231 rexlimdv3a ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \left(\exists {a}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\phantom{\rule{.4em}{0ex}}\left|{G}\left({s}\right)\right|\le {a}\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {d}\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}\right)\right)$
233 96 232 mpd ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {d}\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}\right)$
234 simplll ${⊢}\left(\left(\left({\phi }\wedge {u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\wedge {n}\in ℕ\right)\wedge {s}\in {u}\right)\to {\phi }$
235 simplr ${⊢}\left(\left(\left({\phi }\wedge {u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\wedge {n}\in ℕ\right)\wedge {s}\in {u}\right)\to {n}\in ℕ$
236 simpllr ${⊢}\left(\left(\left({\phi }\wedge {u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\wedge {n}\in ℕ\right)\wedge {s}\in {u}\right)\to {u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
237 simpr ${⊢}\left(\left(\left({\phi }\wedge {u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\wedge {n}\in ℕ\right)\wedge {s}\in {u}\right)\to {s}\in {u}$
238 236 237 sseldd ${⊢}\left(\left(\left({\phi }\wedge {u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\wedge {n}\in ℕ\right)\wedge {s}\in {u}\right)\to {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]$
239 234 235 238 57 syl21anc ${⊢}\left(\left(\left({\phi }\wedge {u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\wedge {n}\in ℕ\right)\wedge {s}\in {u}\right)\to {G}\left({s}\right)={U}\left({s}\right)\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}$
240 239 itgeq2dv ${⊢}\left(\left({\phi }\wedge {u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\wedge {n}\in ℕ\right)\to {\int }_{{u}}{G}\left({s}\right)d{s}={\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}d{s}$
241 240 fveq2d ${⊢}\left(\left({\phi }\wedge {u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\wedge {n}\in ℕ\right)\to \left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|=\left|{\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}d{s}\right|$
242 241 breq1d ${⊢}\left(\left({\phi }\wedge {u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\wedge {n}\in ℕ\right)\to \left(\left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}↔\left|{\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{e}}{2}\right)$
243 242 ralbidva ${⊢}\left({\phi }\wedge {u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}↔\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{e}}{2}\right)$
244 oveq1 ${⊢}{n}={k}\to {n}+\left(\frac{1}{2}\right)={k}+\left(\frac{1}{2}\right)$
245 244 oveq1d ${⊢}{n}={k}\to \left({n}+\left(\frac{1}{2}\right)\right){s}=\left({k}+\left(\frac{1}{2}\right)\right){s}$
246 245 fveq2d ${⊢}{n}={k}\to \mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}=\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}$
247 246 oveq2d ${⊢}{n}={k}\to {U}\left({s}\right)\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}={U}\left({s}\right)\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}$
248 247 adantr ${⊢}\left({n}={k}\wedge {s}\in {u}\right)\to {U}\left({s}\right)\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}={U}\left({s}\right)\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}$
249 248 itgeq2dv ${⊢}{n}={k}\to {\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}d{s}={\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}d{s}$
250 249 fveq2d ${⊢}{n}={k}\to \left|{\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}d{s}\right|=\left|{\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}d{s}\right|$
251 250 breq1d ${⊢}{n}={k}\to \left(\left|{\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{e}}{2}↔\left|{\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{e}}{2}\right)$
252 251 cbvralvw ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{e}}{2}↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{e}}{2}$
253 243 252 syl6bb ${⊢}\left({\phi }\wedge {u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to \left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{e}}{2}\right)$
254 253 adantrr ${⊢}\left({\phi }\wedge \left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {d}\right)\right)\to \left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{e}}{2}\right)$
255 254 pm5.74da ${⊢}{\phi }\to \left(\left(\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {d}\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}\right)↔\left(\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {d}\right)\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{e}}{2}\right)\right)$
256 255 rexralbidv ${⊢}{\phi }\to \left(\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {d}\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}\right)↔\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {d}\right)\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{e}}{2}\right)\right)$
257 256 adantr ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \left(\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {d}\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{G}\left({s}\right)d{s}\right|<\frac{{e}}{2}\right)↔\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {d}\right)\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{e}}{2}\right)\right)$
258 233 257 mpbid ${⊢}\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {u}\in \mathrm{dom}vol\phantom{\rule{.4em}{0ex}}\left(\left({u}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge vol\left({u}\right)\le {d}\right)\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left|{\int }_{{u}}{U}\left({s}\right)\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{e}}{2}\right)$