# Metamath Proof Explorer

## Theorem fourierdlem104

Description: The half upper part of the integral equal to the fourier partial sum, converges to half the right limit of the original function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem104.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
fourierdlem104.xre ${⊢}{\phi }\to {X}\in ℝ$
fourierdlem104.p ${⊢}{P}=\left({m}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {m}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }+{X}\wedge {p}\left({m}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{m}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}\right)$
fourierdlem104.m ${⊢}{\phi }\to {M}\in ℕ$
fourierdlem104.v ${⊢}{\phi }\to {V}\in {P}\left({M}\right)$
fourierdlem104.x ${⊢}{\phi }\to {X}\in \mathrm{ran}{V}$
fourierdlem104.fcn ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
fourierdlem104.fbdioo ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}$
fourierdlem104.fdvcn ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)\underset{cn}{⟶}ℝ$
fourierdlem104.fdvbd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
fourierdlem104.r ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {R}\in \left(\left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right){lim}_{ℂ}{V}\left({i}\right)\right)$
fourierdlem104.l ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {L}\in \left(\left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right){lim}_{ℂ}{V}\left({i}+1\right)\right)$
fourierdlem104.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)$
fourierdlem104.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)$
fourierdlem104.u ${⊢}{U}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{H}\left({s}\right){K}\left({s}\right)\right)$
fourierdlem104.s ${⊢}{S}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right)$
fourierdlem104.g ${⊢}{G}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{U}\left({s}\right){S}\left({s}\right)\right)$
fourierdlem104.z ${⊢}{Z}=\left({m}\in ℕ⟼{\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}\right)$
fourierdlem104.e ${⊢}{E}=\left({n}\in ℕ⟼\frac{{\int }_{\left(0,\mathrm{\pi }\right)}{G}\left({s}\right)d{s}}{\mathrm{\pi }}\right)$
fourierdlem104.y ${⊢}{\phi }\to {Y}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
fourierdlem104.w ${⊢}{\phi }\to {W}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
fourierdlem104.a ${⊢}{\phi }\to {A}\in \left(\left({{{F}}_{ℝ}^{\prime }↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
fourierdlem104.b ${⊢}{\phi }\to {B}\in \left(\left({{{F}}_{ℝ}^{\prime }↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
fourierdlem104.d ${⊢}{D}=\left({n}\in ℕ⟼\left({s}\in ℝ⟼if\left({s}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{n}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)\right)$
fourierdlem104.o ${⊢}{O}={{U}↾}_{\left[{d},\mathrm{\pi }\right]}$
fourierdlem104.t ${⊢}{T}=\left\{{d},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\right)$
fourierdlem104.n ${⊢}{N}=\left|{T}\right|-1$
fourierdlem104.j ${⊢}{J}=\left(\iota {f}|{f}{Isom}_{<,<}\left(\left(0\dots {N}\right),{T}\right)\right)$
fourierdlem104.q ${⊢}{Q}=\left({i}\in \left(0\dots {M}\right)⟼{V}\left({i}\right)-{X}\right)$
fourierdlem104.1 ${⊢}{C}=\left(\iota {l}\in \left(0..^{M}\right)|\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({l}\right),{Q}\left({l}+1\right)\right)\right)$
fourierdlem104.ch ${⊢}{\chi }↔\left(\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in ℕ\right)\wedge \left|{\int }_{\left(0,{d}\right)}{U}\left({s}\right)\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{e}}{2}\right)\wedge \left|{\int }_{\left({d},\mathrm{\pi }\right)}{U}\left({s}\right)\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{e}}{2}\right)$
Assertion fourierdlem104 ${⊢}{\phi }\to {Z}⇝\left(\frac{{Y}}{2}\right)$

### Proof

Step Hyp Ref Expression
1 fourierdlem104.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
2 fourierdlem104.xre ${⊢}{\phi }\to {X}\in ℝ$
3 fourierdlem104.p ${⊢}{P}=\left({m}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {m}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }+{X}\wedge {p}\left({m}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{m}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}\right)$
4 fourierdlem104.m ${⊢}{\phi }\to {M}\in ℕ$
5 fourierdlem104.v ${⊢}{\phi }\to {V}\in {P}\left({M}\right)$
6 fourierdlem104.x ${⊢}{\phi }\to {X}\in \mathrm{ran}{V}$
7 fourierdlem104.fcn ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
8 fourierdlem104.fbdioo ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}$
9 fourierdlem104.fdvcn ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)\underset{cn}{⟶}ℝ$
10 fourierdlem104.fdvbd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
11 fourierdlem104.r ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {R}\in \left(\left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right){lim}_{ℂ}{V}\left({i}\right)\right)$
12 fourierdlem104.l ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {L}\in \left(\left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right){lim}_{ℂ}{V}\left({i}+1\right)\right)$
13 fourierdlem104.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)$
14 fourierdlem104.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)$
15 fourierdlem104.u ${⊢}{U}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{H}\left({s}\right){K}\left({s}\right)\right)$
16 fourierdlem104.s ${⊢}{S}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right)$
17 fourierdlem104.g ${⊢}{G}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{U}\left({s}\right){S}\left({s}\right)\right)$
18 fourierdlem104.z ${⊢}{Z}=\left({m}\in ℕ⟼{\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}\right)$
19 fourierdlem104.e ${⊢}{E}=\left({n}\in ℕ⟼\frac{{\int }_{\left(0,\mathrm{\pi }\right)}{G}\left({s}\right)d{s}}{\mathrm{\pi }}\right)$
20 fourierdlem104.y ${⊢}{\phi }\to {Y}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
21 fourierdlem104.w ${⊢}{\phi }\to {W}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
22 fourierdlem104.a ${⊢}{\phi }\to {A}\in \left(\left({{{F}}_{ℝ}^{\prime }↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
23 fourierdlem104.b ${⊢}{\phi }\to {B}\in \left(\left({{{F}}_{ℝ}^{\prime }↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
24 fourierdlem104.d ${⊢}{D}=\left({n}\in ℕ⟼\left({s}\in ℝ⟼if\left({s}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{n}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)\right)$
25 fourierdlem104.o ${⊢}{O}={{U}↾}_{\left[{d},\mathrm{\pi }\right]}$
26 fourierdlem104.t ${⊢}{T}=\left\{{d},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\right)$
27 fourierdlem104.n ${⊢}{N}=\left|{T}\right|-1$
28 fourierdlem104.j ${⊢}{J}=\left(\iota {f}|{f}{Isom}_{<,<}\left(\left(0\dots {N}\right),{T}\right)\right)$
29 fourierdlem104.q ${⊢}{Q}=\left({i}\in \left(0\dots {M}\right)⟼{V}\left({i}\right)-{X}\right)$
30 fourierdlem104.1 ${⊢}{C}=\left(\iota {l}\in \left(0..^{M}\right)|\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({l}\right),{Q}\left({l}+1\right)\right)\right)$
31 fourierdlem104.ch ${⊢}{\chi }↔\left(\left(\left(\left(\left({\phi }\wedge {e}\in {ℝ}^{+}\right)\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in ℕ\right)\wedge \left|{\int }_{\left(0,{d}\right)}{U}\left({s}\right)\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{e}}{2}\right)\wedge \left|{\int }_{\left({d},\mathrm{\pi }\right)}{U}\left({s}\right)\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{e}}{2}\right)$
32 eqid ${⊢}{ℤ}_{\ge 1}={ℤ}_{\ge 1}$
33 1zzd ${⊢}{\phi }\to 1\in ℤ$
34 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{\phi }$
35 nfmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼{\int }_{\left(0,\mathrm{\pi }\right)}{G}\left({s}\right)d{s}\right)$
36 nfmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼\mathrm{\pi }\right)$
37 nfmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼\frac{{\int }_{\left(0,\mathrm{\pi }\right)}{G}\left({s}\right)d{s}}{\mathrm{\pi }}\right)$
38 19 37 nfcxfr ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{E}$
39 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
40 elioore ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to {d}\in ℝ$
41 40 adantl ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {d}\in ℝ$
42 pire ${⊢}\mathrm{\pi }\in ℝ$
43 42 a1i ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \mathrm{\pi }\in ℝ$
44 ioossre ${⊢}\left({X},\mathrm{+\infty }\right)\subseteq ℝ$
45 44 a1i ${⊢}{\phi }\to \left({X},\mathrm{+\infty }\right)\subseteq ℝ$
46 1 45 fssresd ${⊢}{\phi }\to \left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right):\left({X},\mathrm{+\infty }\right)⟶ℝ$
47 ioosscn ${⊢}\left({X},\mathrm{+\infty }\right)\subseteq ℂ$
48 47 a1i ${⊢}{\phi }\to \left({X},\mathrm{+\infty }\right)\subseteq ℂ$
49 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
50 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
51 50 a1i ${⊢}{\phi }\to \mathrm{+\infty }\in {ℝ}^{*}$
52 2 ltpnfd ${⊢}{\phi }\to {X}<\mathrm{+\infty }$
53 49 51 2 52 lptioo1cn ${⊢}{\phi }\to {X}\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(\left({X},\mathrm{+\infty }\right)\right)$
54 46 48 53 20 limcrecl ${⊢}{\phi }\to {Y}\in ℝ$
55 ioossre ${⊢}\left(\mathrm{-\infty },{X}\right)\subseteq ℝ$
56 55 a1i ${⊢}{\phi }\to \left(\mathrm{-\infty },{X}\right)\subseteq ℝ$
57 1 56 fssresd ${⊢}{\phi }\to \left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right):\left(\mathrm{-\infty },{X}\right)⟶ℝ$
58 ioosscn ${⊢}\left(\mathrm{-\infty },{X}\right)\subseteq ℂ$
59 58 a1i ${⊢}{\phi }\to \left(\mathrm{-\infty },{X}\right)\subseteq ℂ$
60 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
61 60 a1i ${⊢}{\phi }\to \mathrm{-\infty }\in {ℝ}^{*}$
62 2 mnfltd ${⊢}{\phi }\to \mathrm{-\infty }<{X}$
63 49 61 2 62 lptioo2cn ${⊢}{\phi }\to {X}\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(\left(\mathrm{-\infty },{X}\right)\right)$
64 57 59 63 21 limcrecl ${⊢}{\phi }\to {W}\in ℝ$
65 1 2 54 64 13 14 15 fourierdlem55 ${⊢}{\phi }\to {U}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
66 ax-resscn ${⊢}ℝ\subseteq ℂ$
67 66 a1i ${⊢}{\phi }\to ℝ\subseteq ℂ$
68 65 67 fssd ${⊢}{\phi }\to {U}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℂ$
69 68 adantr ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {U}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℂ$
70 42 renegcli ${⊢}-\mathrm{\pi }\in ℝ$
71 70 a1i ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to -\mathrm{\pi }\in ℝ$
72 70 a1i ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to -\mathrm{\pi }\in ℝ$
73 0red ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to 0\in ℝ$
74 negpilt0 ${⊢}-\mathrm{\pi }<0$
75 74 a1i ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to -\mathrm{\pi }<0$
76 0xr ${⊢}0\in {ℝ}^{*}$
77 42 rexri ${⊢}\mathrm{\pi }\in {ℝ}^{*}$
78 ioogtlb ${⊢}\left(0\in {ℝ}^{*}\wedge \mathrm{\pi }\in {ℝ}^{*}\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to 0<{d}$
79 76 77 78 mp3an12 ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to 0<{d}$
80 72 73 40 75 79 lttrd ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to -\mathrm{\pi }<{d}$
81 72 40 80 ltled ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to -\mathrm{\pi }\le {d}$
82 81 adantl ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to -\mathrm{\pi }\le {d}$
83 43 leidd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \mathrm{\pi }\le \mathrm{\pi }$
84 iccss ${⊢}\left(\left(-\mathrm{\pi }\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\wedge \left(-\mathrm{\pi }\le {d}\wedge \mathrm{\pi }\le \mathrm{\pi }\right)\right)\to \left[{d},\mathrm{\pi }\right]\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
85 71 43 82 83 84 syl22anc ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \left[{d},\mathrm{\pi }\right]\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
86 69 85 fssresd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \left({{U}↾}_{\left[{d},\mathrm{\pi }\right]}\right):\left[{d},\mathrm{\pi }\right]⟶ℂ$
87 25 a1i ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {O}={{U}↾}_{\left[{d},\mathrm{\pi }\right]}$
88 87 feq1d ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \left({O}:\left[{d},\mathrm{\pi }\right]⟶ℂ↔\left({{U}↾}_{\left[{d},\mathrm{\pi }\right]}\right):\left[{d},\mathrm{\pi }\right]⟶ℂ\right)$
89 86 88 mpbird ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {O}:\left[{d},\mathrm{\pi }\right]⟶ℂ$
90 42 elexi ${⊢}\mathrm{\pi }\in \mathrm{V}$
91 90 prid2 ${⊢}\mathrm{\pi }\in \left\{{d},\mathrm{\pi }\right\}$
92 elun1 ${⊢}\mathrm{\pi }\in \left\{{d},\mathrm{\pi }\right\}\to \mathrm{\pi }\in \left(\left\{{d},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\right)\right)$
93 91 92 ax-mp ${⊢}\mathrm{\pi }\in \left(\left\{{d},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\right)\right)$
94 93 26 eleqtrri ${⊢}\mathrm{\pi }\in {T}$
95 94 ne0ii ${⊢}{T}\ne \varnothing$
96 95 a1i ${⊢}{\phi }\to {T}\ne \varnothing$
97 prfi ${⊢}\left\{{d},\mathrm{\pi }\right\}\in \mathrm{Fin}$
98 97 a1i ${⊢}{\phi }\to \left\{{d},\mathrm{\pi }\right\}\in \mathrm{Fin}$
99 fzfi ${⊢}\left(0\dots {M}\right)\in \mathrm{Fin}$
100 29 rnmptfi ${⊢}\left(0\dots {M}\right)\in \mathrm{Fin}\to \mathrm{ran}{Q}\in \mathrm{Fin}$
101 99 100 ax-mp ${⊢}\mathrm{ran}{Q}\in \mathrm{Fin}$
102 infi ${⊢}\mathrm{ran}{Q}\in \mathrm{Fin}\to \mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\in \mathrm{Fin}$
103 101 102 mp1i ${⊢}{\phi }\to \mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\in \mathrm{Fin}$
104 unfi ${⊢}\left(\left\{{d},\mathrm{\pi }\right\}\in \mathrm{Fin}\wedge \mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\in \mathrm{Fin}\right)\to \left\{{d},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\right)\in \mathrm{Fin}$
105 98 103 104 syl2anc ${⊢}{\phi }\to \left\{{d},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\right)\in \mathrm{Fin}$
106 26 105 eqeltrid ${⊢}{\phi }\to {T}\in \mathrm{Fin}$
107 hashnncl ${⊢}{T}\in \mathrm{Fin}\to \left(\left|{T}\right|\in ℕ↔{T}\ne \varnothing \right)$
108 106 107 syl ${⊢}{\phi }\to \left(\left|{T}\right|\in ℕ↔{T}\ne \varnothing \right)$
109 96 108 mpbird ${⊢}{\phi }\to \left|{T}\right|\in ℕ$
110 nnm1nn0 ${⊢}\left|{T}\right|\in ℕ\to \left|{T}\right|-1\in {ℕ}_{0}$
111 109 110 syl ${⊢}{\phi }\to \left|{T}\right|-1\in {ℕ}_{0}$
112 27 111 eqeltrid ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
113 112 adantr ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {N}\in {ℕ}_{0}$
114 0red ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to 0\in ℝ$
115 1red ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to 1\in ℝ$
116 113 nn0red ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {N}\in ℝ$
117 0lt1 ${⊢}0<1$
118 117 a1i ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to 0<1$
119 2re ${⊢}2\in ℝ$
120 119 a1i ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to 2\in ℝ$
121 109 nnred ${⊢}{\phi }\to \left|{T}\right|\in ℝ$
122 121 adantr ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \left|{T}\right|\in ℝ$
123 iooltub ${⊢}\left(0\in {ℝ}^{*}\wedge \mathrm{\pi }\in {ℝ}^{*}\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {d}<\mathrm{\pi }$
124 76 77 123 mp3an12 ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to {d}<\mathrm{\pi }$
125 40 124 ltned ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to {d}\ne \mathrm{\pi }$
126 125 adantl ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {d}\ne \mathrm{\pi }$
127 hashprg ${⊢}\left({d}\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \left({d}\ne \mathrm{\pi }↔\left|\left\{{d},\mathrm{\pi }\right\}\right|=2\right)$
128 41 42 127 sylancl ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \left({d}\ne \mathrm{\pi }↔\left|\left\{{d},\mathrm{\pi }\right\}\right|=2\right)$
129 126 128 mpbid ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \left|\left\{{d},\mathrm{\pi }\right\}\right|=2$
130 129 eqcomd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to 2=\left|\left\{{d},\mathrm{\pi }\right\}\right|$
131 106 adantr ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {T}\in \mathrm{Fin}$
132 ssun1 ${⊢}\left\{{d},\mathrm{\pi }\right\}\subseteq \left\{{d},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\right)$
133 132 26 sseqtrri ${⊢}\left\{{d},\mathrm{\pi }\right\}\subseteq {T}$
134 hashssle ${⊢}\left({T}\in \mathrm{Fin}\wedge \left\{{d},\mathrm{\pi }\right\}\subseteq {T}\right)\to \left|\left\{{d},\mathrm{\pi }\right\}\right|\le \left|{T}\right|$
135 131 133 134 sylancl ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \left|\left\{{d},\mathrm{\pi }\right\}\right|\le \left|{T}\right|$
136 130 135 eqbrtrd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to 2\le \left|{T}\right|$
137 120 122 115 136 lesub1dd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to 2-1\le \left|{T}\right|-1$
138 1e2m1 ${⊢}1=2-1$
139 137 138 27 3brtr4g ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to 1\le {N}$
140 114 115 116 118 139 ltletrd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to 0<{N}$
141 140 gt0ne0d ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {N}\ne 0$
142 elnnne0 ${⊢}{N}\in ℕ↔\left({N}\in {ℕ}_{0}\wedge {N}\ne 0\right)$
143 113 141 142 sylanbrc ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {N}\in ℕ$
144 41 leidd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {d}\le {d}$
145 42 a1i ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to \mathrm{\pi }\in ℝ$
146 40 145 124 ltled ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to {d}\le \mathrm{\pi }$
147 146 adantl ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {d}\le \mathrm{\pi }$
148 41 43 41 144 147 eliccd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {d}\in \left[{d},\mathrm{\pi }\right]$
149 41 43 43 147 83 eliccd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \mathrm{\pi }\in \left[{d},\mathrm{\pi }\right]$
150 148 149 jca ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \left({d}\in \left[{d},\mathrm{\pi }\right]\wedge \mathrm{\pi }\in \left[{d},\mathrm{\pi }\right]\right)$
151 vex ${⊢}{d}\in \mathrm{V}$
152 151 90 prss ${⊢}\left({d}\in \left[{d},\mathrm{\pi }\right]\wedge \mathrm{\pi }\in \left[{d},\mathrm{\pi }\right]\right)↔\left\{{d},\mathrm{\pi }\right\}\subseteq \left[{d},\mathrm{\pi }\right]$
153 150 152 sylib ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \left\{{d},\mathrm{\pi }\right\}\subseteq \left[{d},\mathrm{\pi }\right]$
154 inss2 ${⊢}\mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\subseteq \left({d},\mathrm{\pi }\right)$
155 154 a1i ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\subseteq \left({d},\mathrm{\pi }\right)$
156 ioossicc ${⊢}\left({d},\mathrm{\pi }\right)\subseteq \left[{d},\mathrm{\pi }\right]$
157 155 156 sstrdi ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\subseteq \left[{d},\mathrm{\pi }\right]$
158 153 157 unssd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \left\{{d},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\right)\subseteq \left[{d},\mathrm{\pi }\right]$
159 26 158 eqsstrid ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {T}\subseteq \left[{d},\mathrm{\pi }\right]$
160 151 prid1 ${⊢}{d}\in \left\{{d},\mathrm{\pi }\right\}$
161 elun1 ${⊢}{d}\in \left\{{d},\mathrm{\pi }\right\}\to {d}\in \left(\left\{{d},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\right)\right)$
162 160 161 ax-mp ${⊢}{d}\in \left(\left\{{d},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\right)\right)$
163 162 26 eleqtrri ${⊢}{d}\in {T}$
164 163 a1i ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {d}\in {T}$
165 94 a1i ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \mathrm{\pi }\in {T}$
166 131 27 28 41 43 159 164 165 fourierdlem52 ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \left(\left({J}:\left(0\dots {N}\right)⟶\left[{d},\mathrm{\pi }\right]\wedge {J}\left(0\right)={d}\right)\wedge {J}\left({N}\right)=\mathrm{\pi }\right)$
167 166 simplld ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {J}:\left(0\dots {N}\right)⟶\left[{d},\mathrm{\pi }\right]$
168 166 simplrd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {J}\left(0\right)={d}$
169 166 simprd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {J}\left({N}\right)=\mathrm{\pi }$
170 elfzoelz ${⊢}{k}\in \left(0..^{N}\right)\to {k}\in ℤ$
171 170 zred ${⊢}{k}\in \left(0..^{N}\right)\to {k}\in ℝ$
172 171 adantl ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {k}\in ℝ$
173 172 ltp1d ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {k}<{k}+1$
174 40 145 jca ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to \left({d}\in ℝ\wedge \mathrm{\pi }\in ℝ\right)$
175 151 90 prss ${⊢}\left({d}\in ℝ\wedge \mathrm{\pi }\in ℝ\right)↔\left\{{d},\mathrm{\pi }\right\}\subseteq ℝ$
176 174 175 sylib ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to \left\{{d},\mathrm{\pi }\right\}\subseteq ℝ$
177 176 adantl ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \left\{{d},\mathrm{\pi }\right\}\subseteq ℝ$
178 ioossre ${⊢}\left({d},\mathrm{\pi }\right)\subseteq ℝ$
179 154 178 sstri ${⊢}\mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\subseteq ℝ$
180 179 a1i ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\subseteq ℝ$
181 177 180 unssd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \left\{{d},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}{Q}\cap \left({d},\mathrm{\pi }\right)\right)\subseteq ℝ$
182 26 181 eqsstrid ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {T}\subseteq ℝ$
183 131 182 28 27 fourierdlem36 ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {J}{Isom}_{<,<}\left(\left(0\dots {N}\right),{T}\right)$
184 183 adantr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {J}{Isom}_{<,<}\left(\left(0\dots {N}\right),{T}\right)$
185 elfzofz ${⊢}{k}\in \left(0..^{N}\right)\to {k}\in \left(0\dots {N}\right)$
186 185 adantl ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {k}\in \left(0\dots {N}\right)$
187 fzofzp1 ${⊢}{k}\in \left(0..^{N}\right)\to {k}+1\in \left(0\dots {N}\right)$
188 187 adantl ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {k}+1\in \left(0\dots {N}\right)$
189 isorel ${⊢}\left({J}{Isom}_{<,<}\left(\left(0\dots {N}\right),{T}\right)\wedge \left({k}\in \left(0\dots {N}\right)\wedge {k}+1\in \left(0\dots {N}\right)\right)\right)\to \left({k}<{k}+1↔{J}\left({k}\right)<{J}\left({k}+1\right)\right)$
190 184 186 188 189 syl12anc ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({k}<{k}+1↔{J}\left({k}\right)<{J}\left({k}+1\right)\right)$
191 173 190 mpbid ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {J}\left({k}\right)<{J}\left({k}+1\right)$
192 65 adantr ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {U}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
193 192 85 feqresmpt ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {{U}↾}_{\left[{d},\mathrm{\pi }\right]}=\left({s}\in \left[{d},\mathrm{\pi }\right]⟼{U}\left({s}\right)\right)$
194 85 sselda ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]$
195 1 2 54 64 13 fourierdlem9 ${⊢}{\phi }\to {H}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
196 195 ad2antrr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {H}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
197 196 194 ffvelrnd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {H}\left({s}\right)\in ℝ$
198 14 fourierdlem43 ${⊢}{K}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
199 198 a1i ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {K}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
200 199 194 ffvelrnd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {K}\left({s}\right)\in ℝ$
201 197 200 remulcld ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {H}\left({s}\right){K}\left({s}\right)\in ℝ$
202 15 fvmpt2 ${⊢}\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge {H}\left({s}\right){K}\left({s}\right)\in ℝ\right)\to {U}\left({s}\right)={H}\left({s}\right){K}\left({s}\right)$
203 194 201 202 syl2anc ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {U}\left({s}\right)={H}\left({s}\right){K}\left({s}\right)$
204 0red ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to 0\in ℝ$
205 40 adantr ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {d}\in ℝ$
206 42 a1i ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to \mathrm{\pi }\in ℝ$
207 simpr ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {s}\in \left[{d},\mathrm{\pi }\right]$
208 eliccre ${⊢}\left({d}\in ℝ\wedge \mathrm{\pi }\in ℝ\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {s}\in ℝ$
209 205 206 207 208 syl3anc ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {s}\in ℝ$
210 79 adantr ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to 0<{d}$
211 205 rexrd ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {d}\in {ℝ}^{*}$
212 77 a1i ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to \mathrm{\pi }\in {ℝ}^{*}$
213 iccgelb ${⊢}\left({d}\in {ℝ}^{*}\wedge \mathrm{\pi }\in {ℝ}^{*}\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {d}\le {s}$
214 211 212 207 213 syl3anc ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {d}\le {s}$
215 204 205 209 210 214 ltletrd ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to 0<{s}$
216 215 gt0ne0d ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {s}\ne 0$
217 216 adantll ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {s}\ne 0$
218 217 neneqd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to ¬{s}=0$
219 218 iffalsed ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to if\left({s}=0,0,\frac{{F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)}{{s}}\right)=\frac{{F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)}{{s}}$
220 215 adantll ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to 0<{s}$
221 220 iftrued ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to if\left(0<{s},{Y},{W}\right)={Y}$
222 221 oveq2d ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)={F}\left({X}+{s}\right)-{Y}$
223 222 oveq1d ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to \frac{{F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)}{{s}}=\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}$
224 219 223 eqtrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to if\left({s}=0,0,\frac{{F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)}{{s}}\right)=\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}$
225 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {F}:ℝ⟶ℝ$
226 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {X}\in ℝ$
227 iccssre ${⊢}\left(-\mathrm{\pi }\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \left[-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℝ$
228 70 42 227 mp2an ${⊢}\left[-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℝ$
229 228 194 sseldi ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {s}\in ℝ$
230 226 229 readdcld ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {X}+{s}\in ℝ$
231 225 230 ffvelrnd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {F}\left({X}+{s}\right)\in ℝ$
232 54 ad2antrr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {Y}\in ℝ$
233 231 232 resubcld ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {F}\left({X}+{s}\right)-{Y}\in ℝ$
234 233 229 217 redivcld ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to \frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\in ℝ$
235 224 234 eqeltrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to if\left({s}=0,0,\frac{{F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)}{{s}}\right)\in ℝ$
236 13 fvmpt2 ${⊢}\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge if\left({s}=0,0,\frac{{F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)}{{s}}\right)\in ℝ\right)\to {H}\left({s}\right)=if\left({s}=0,0,\frac{{F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)}{{s}}\right)$
237 194 235 236 syl2anc ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {H}\left({s}\right)=if\left({s}=0,0,\frac{{F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)}{{s}}\right)$
238 237 219 223 3eqtrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {H}\left({s}\right)=\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}$
239 206 renegcld ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to -\mathrm{\pi }\in ℝ$
240 74 a1i ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to -\mathrm{\pi }<0$
241 239 204 209 240 215 lttrd ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to -\mathrm{\pi }<{s}$
242 239 209 241 ltled ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to -\mathrm{\pi }\le {s}$
243 iccleub ${⊢}\left({d}\in {ℝ}^{*}\wedge \mathrm{\pi }\in {ℝ}^{*}\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {s}\le \mathrm{\pi }$
244 211 212 207 243 syl3anc ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {s}\le \mathrm{\pi }$
245 239 206 209 242 244 eliccd ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]$
246 216 neneqd ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to ¬{s}=0$
247 246 iffalsed ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to if\left({s}=0,1,\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)=\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}$
248 119 a1i ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to 2\in ℝ$
249 209 rehalfcld ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to \frac{{s}}{2}\in ℝ$
250 249 resincld ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to \mathrm{sin}\left(\frac{{s}}{2}\right)\in ℝ$
251 248 250 remulcld ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to 2\mathrm{sin}\left(\frac{{s}}{2}\right)\in ℝ$
252 2cnd ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to 2\in ℂ$
253 209 recnd ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {s}\in ℂ$
254 253 halfcld ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to \frac{{s}}{2}\in ℂ$
255 254 sincld ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to \mathrm{sin}\left(\frac{{s}}{2}\right)\in ℂ$
256 2ne0 ${⊢}2\ne 0$
257 256 a1i ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to 2\ne 0$
258 fourierdlem44 ${⊢}\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge {s}\ne 0\right)\to \mathrm{sin}\left(\frac{{s}}{2}\right)\ne 0$
259 245 216 258 syl2anc ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to \mathrm{sin}\left(\frac{{s}}{2}\right)\ne 0$
260 252 255 257 259 mulne0d ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to 2\mathrm{sin}\left(\frac{{s}}{2}\right)\ne 0$
261 209 251 260 redivcld ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to \frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\in ℝ$
262 247 261 eqeltrd ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to if\left({s}=0,1,\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\in ℝ$
263 14 fvmpt2 ${⊢}\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge if\left({s}=0,1,\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\in ℝ\right)\to {K}\left({s}\right)=if\left({s}=0,1,\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
264 245 262 263 syl2anc ${⊢}\left({d}\in \left(0,\mathrm{\pi }\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {K}\left({s}\right)=if\left({s}=0,1,\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
265 264 adantll ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {K}\left({s}\right)=if\left({s}=0,1,\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
266 238 265 oveq12d ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {H}\left({s}\right){K}\left({s}\right)=\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)if\left({s}=0,1,\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
267 218 iffalsed ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to if\left({s}=0,1,\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)=\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}$
268 267 oveq2d ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to \left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)if\left({s}=0,1,\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)=\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
269 203 266 268 3eqtrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {U}\left({s}\right)=\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
270 269 mpteq2dva ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \left({s}\in \left[{d},\mathrm{\pi }\right]⟼{U}\left({s}\right)\right)=\left({s}\in \left[{d},\mathrm{\pi }\right]⟼\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)$
271 87 193 270 3eqtrd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {O}=\left({s}\in \left[{d},\mathrm{\pi }\right]⟼\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)$
272 271 adantr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {O}=\left({s}\in \left[{d},\mathrm{\pi }\right]⟼\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)$
273 272 reseq1d ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {{O}↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}={\left({s}\in \left[{d},\mathrm{\pi }\right]⟼\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}$
274 1 adantr ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {F}:ℝ⟶ℝ$
275 2 adantr ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {X}\in ℝ$
276 4 adantr ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {M}\in ℕ$
277 5 adantr ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {V}\in {P}\left({M}\right)$
278 7 adantlr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
279 11 adantlr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {R}\in \left(\left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right){lim}_{ℂ}{V}\left({i}\right)\right)$
280 12 adantlr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {L}\in \left(\left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right){lim}_{ℂ}{V}\left({i}+1\right)\right)$
281 124 adantl ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {d}<\mathrm{\pi }$
282 73 40 ltnled ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to \left(0<{d}↔¬{d}\le 0\right)$
283 79 282 mpbid ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to ¬{d}\le 0$
284 283 intn3an2d ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to ¬\left(0\in ℝ\wedge {d}\le 0\wedge 0\le \mathrm{\pi }\right)$
285 elicc2 ${⊢}\left({d}\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \left(0\in \left[{d},\mathrm{\pi }\right]↔\left(0\in ℝ\wedge {d}\le 0\wedge 0\le \mathrm{\pi }\right)\right)$
286 40 42 285 sylancl ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to \left(0\in \left[{d},\mathrm{\pi }\right]↔\left(0\in ℝ\wedge {d}\le 0\wedge 0\le \mathrm{\pi }\right)\right)$
287 284 286 mtbird ${⊢}{d}\in \left(0,\mathrm{\pi }\right)\to ¬0\in \left[{d},\mathrm{\pi }\right]$
288 287 adantl ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to ¬0\in \left[{d},\mathrm{\pi }\right]$
289 54 adantr ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {Y}\in ℝ$
290 eqid ${⊢}\left({s}\in \left[{d},\mathrm{\pi }\right]⟼\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)=\left({s}\in \left[{d},\mathrm{\pi }\right]⟼\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)$
291 eqid
292 eqid
293 fveq2 ${⊢}{l}={i}\to {Q}\left({l}\right)={Q}\left({i}\right)$
294 oveq1 ${⊢}{l}={i}\to {l}+1={i}+1$
295 294 fveq2d ${⊢}{l}={i}\to {Q}\left({l}+1\right)={Q}\left({i}+1\right)$
296 293 295 oveq12d ${⊢}{l}={i}\to \left({Q}\left({l}\right),{Q}\left({l}+1\right)\right)=\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)$
297 296 sseq2d ${⊢}{l}={i}\to \left(\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({l}\right),{Q}\left({l}+1\right)\right)↔\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)$
298 297 cbvriotavw ${⊢}\left(\iota {l}\in \left(0..^{M}\right)|\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({l}\right),{Q}\left({l}+1\right)\right)\right)=\left(\iota {i}\in \left(0..^{M}\right)|\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)$
299 274 275 3 276 277 278 279 280 41 43 281 85 288 289 290 29 26 27 28 291 292 298 fourierdlem86
300 299 simprd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({\left({s}\in \left[{d},\mathrm{\pi }\right]⟼\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}\right):\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\underset{cn}{⟶}ℂ$
301 273 300 eqeltrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({{O}↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}\right):\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\underset{cn}{⟶}ℂ$
302 299 simplld
303 272 eqcomd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({s}\in \left[{d},\mathrm{\pi }\right]⟼\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)={O}$
304 303 reseq1d ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {\left({s}\in \left[{d},\mathrm{\pi }\right]⟼\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}={{O}↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}$
305 304 oveq1d ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({\left({s}\in \left[{d},\mathrm{\pi }\right]⟼\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}\right){lim}_{ℂ}{J}\left({k}+1\right)=\left({{O}↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}\right){lim}_{ℂ}{J}\left({k}+1\right)$
306 302 305 eleqtrd
307 299 simplrd
308 304 oveq1d ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({\left({s}\in \left[{d},\mathrm{\pi }\right]⟼\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}\right){lim}_{ℂ}{J}\left({k}\right)=\left({{O}↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}\right){lim}_{ℂ}{J}\left({k}\right)$
309 307 308 eleqtrd
310 eqid ${⊢}ℝ\mathrm{D}{O}=ℝ\mathrm{D}{O}$
311 89 adantr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {O}:\left[{d},\mathrm{\pi }\right]⟶ℂ$
312 41 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {d}\in ℝ$
313 42 a1i ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to \mathrm{\pi }\in ℝ$
314 elioore ${⊢}{s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\to {s}\in ℝ$
315 314 adantl ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {s}\in ℝ$
316 85 228 sstrdi ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \left[{d},\mathrm{\pi }\right]\subseteq ℝ$
317 316 adantr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left[{d},\mathrm{\pi }\right]\subseteq ℝ$
318 167 adantr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {J}:\left(0\dots {N}\right)⟶\left[{d},\mathrm{\pi }\right]$
319 318 186 ffvelrnd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {J}\left({k}\right)\in \left[{d},\mathrm{\pi }\right]$
320 317 319 sseldd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {J}\left({k}\right)\in ℝ$
321 320 adantr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {J}\left({k}\right)\in ℝ$
322 41 adantr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {d}\in ℝ$
323 322 rexrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {d}\in {ℝ}^{*}$
324 77 a1i ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \mathrm{\pi }\in {ℝ}^{*}$
325 iccgelb ${⊢}\left({d}\in {ℝ}^{*}\wedge \mathrm{\pi }\in {ℝ}^{*}\wedge {J}\left({k}\right)\in \left[{d},\mathrm{\pi }\right]\right)\to {d}\le {J}\left({k}\right)$
326 323 324 319 325 syl3anc ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {d}\le {J}\left({k}\right)$
327 326 adantr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {d}\le {J}\left({k}\right)$
328 321 rexrd ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {J}\left({k}\right)\in {ℝ}^{*}$
329 318 188 ffvelrnd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {J}\left({k}+1\right)\in \left[{d},\mathrm{\pi }\right]$
330 317 329 sseldd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {J}\left({k}+1\right)\in ℝ$
331 330 rexrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {J}\left({k}+1\right)\in {ℝ}^{*}$
332 331 adantr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {J}\left({k}+1\right)\in {ℝ}^{*}$
333 simpr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)$
334 ioogtlb ${⊢}\left({J}\left({k}\right)\in {ℝ}^{*}\wedge {J}\left({k}+1\right)\in {ℝ}^{*}\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {J}\left({k}\right)<{s}$
335 328 332 333 334 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {J}\left({k}\right)<{s}$
336 312 321 315 327 335 lelttrd ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {d}<{s}$
337 312 315 336 ltled ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {d}\le {s}$
338 330 adantr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {J}\left({k}+1\right)\in ℝ$
339 iooltub ${⊢}\left({J}\left({k}\right)\in {ℝ}^{*}\wedge {J}\left({k}+1\right)\in {ℝ}^{*}\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {s}<{J}\left({k}+1\right)$
340 328 332 333 339 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {s}<{J}\left({k}+1\right)$
341 iccleub ${⊢}\left({d}\in {ℝ}^{*}\wedge \mathrm{\pi }\in {ℝ}^{*}\wedge {J}\left({k}+1\right)\in \left[{d},\mathrm{\pi }\right]\right)\to {J}\left({k}+1\right)\le \mathrm{\pi }$
342 323 324 329 341 syl3anc ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {J}\left({k}+1\right)\le \mathrm{\pi }$
343 342 adantr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {J}\left({k}+1\right)\le \mathrm{\pi }$
344 315 338 313 340 343 ltletrd ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {s}<\mathrm{\pi }$
345 315 313 344 ltled ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {s}\le \mathrm{\pi }$
346 312 313 315 337 345 eliccd ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {s}\in \left[{d},\mathrm{\pi }\right]$
347 346 ralrimiva ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \forall {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}{s}\in \left[{d},\mathrm{\pi }\right]$
348 dfss3 ${⊢}\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left[{d},\mathrm{\pi }\right]↔\forall {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}{s}\in \left[{d},\mathrm{\pi }\right]$
349 347 348 sylibr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left[{d},\mathrm{\pi }\right]$
350 311 349 feqresmpt ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {{O}↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}=\left({s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼{O}\left({s}\right)\right)$
351 simplll ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {\phi }$
352 simpllr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {d}\in \left(0,\mathrm{\pi }\right)$
353 25 fveq1i ${⊢}{O}\left({s}\right)=\left({{U}↾}_{\left[{d},\mathrm{\pi }\right]}\right)\left({s}\right)$
354 353 a1i ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {O}\left({s}\right)=\left({{U}↾}_{\left[{d},\mathrm{\pi }\right]}\right)\left({s}\right)$
355 fvres ${⊢}{s}\in \left[{d},\mathrm{\pi }\right]\to \left({{U}↾}_{\left[{d},\mathrm{\pi }\right]}\right)\left({s}\right)={U}\left({s}\right)$
356 355 adantl ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to \left({{U}↾}_{\left[{d},\mathrm{\pi }\right]}\right)\left({s}\right)={U}\left({s}\right)$
357 265 267 eqtrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {K}\left({s}\right)=\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}$
358 238 357 oveq12d ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {H}\left({s}\right){K}\left({s}\right)=\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
359 233 recnd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {F}\left({X}+{s}\right)-{Y}\in ℂ$
360 253 adantll ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {s}\in ℂ$
361 2cnd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to 2\in ℂ$
362 360 halfcld ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to \frac{{s}}{2}\in ℂ$
363 362 sincld ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to \mathrm{sin}\left(\frac{{s}}{2}\right)\in ℂ$
364 361 363 mulcld ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to 2\mathrm{sin}\left(\frac{{s}}{2}\right)\in ℂ$
365 260 adantll ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to 2\mathrm{sin}\left(\frac{{s}}{2}\right)\ne 0$
366 359 360 364 217 365 dmdcan2d ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to \left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)=\frac{{F}\left({X}+{s}\right)-{Y}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}$
367 203 358 366 3eqtrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {U}\left({s}\right)=\frac{{F}\left({X}+{s}\right)-{Y}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}$
368 354 356 367 3eqtrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {s}\in \left[{d},\mathrm{\pi }\right]\right)\to {O}\left({s}\right)=\frac{{F}\left({X}+{s}\right)-{Y}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}$
369 351 352 346 368 syl21anc ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {O}\left({s}\right)=\frac{{F}\left({X}+{s}\right)-{Y}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}$
370 351 352 346 366 syl21anc ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to \left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)=\frac{{F}\left({X}+{s}\right)-{Y}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}$
371 370 eqcomd ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to \frac{{F}\left({X}+{s}\right)-{Y}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}=\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
372 eqidd ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to \left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{t}\right)-{Y}}{{t}}\right)=\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{t}\right)-{Y}}{{t}}\right)$
373 oveq2 ${⊢}{t}={s}\to {X}+{t}={X}+{s}$
374 373 fveq2d ${⊢}{t}={s}\to {F}\left({X}+{t}\right)={F}\left({X}+{s}\right)$
375 374 oveq1d ${⊢}{t}={s}\to {F}\left({X}+{t}\right)-{Y}={F}\left({X}+{s}\right)-{Y}$
376 id ${⊢}{t}={s}\to {t}={s}$
377 375 376 oveq12d ${⊢}{t}={s}\to \frac{{F}\left({X}+{t}\right)-{Y}}{{t}}=\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}$
378 377 adantl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\wedge {t}={s}\right)\to \frac{{F}\left({X}+{t}\right)-{Y}}{{t}}=\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}$
379 simpr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)$
380 ovex ${⊢}\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\in \mathrm{V}$
381 380 a1i ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to \frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\in \mathrm{V}$
382 372 378 379 381 fvmptd ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to \left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{t}\right)-{Y}}{{t}}\right)\left({s}\right)=\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}$
383 eqidd ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to \left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{t}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}\right)=\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{t}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}\right)$
384 oveq1 ${⊢}{t}={s}\to \frac{{t}}{2}=\frac{{s}}{2}$
385 384 fveq2d ${⊢}{t}={s}\to \mathrm{sin}\left(\frac{{t}}{2}\right)=\mathrm{sin}\left(\frac{{s}}{2}\right)$
386 385 oveq2d ${⊢}{t}={s}\to 2\mathrm{sin}\left(\frac{{t}}{2}\right)=2\mathrm{sin}\left(\frac{{s}}{2}\right)$
387 376 386 oveq12d ${⊢}{t}={s}\to \frac{{t}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}=\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}$
388 387 adantl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\wedge {t}={s}\right)\to \frac{{t}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}=\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}$
389 ovex ${⊢}\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\in \mathrm{V}$
390 389 a1i ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to \frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\in \mathrm{V}$
391 383 388 379 390 fvmptd ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to \left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{t}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}\right)\left({s}\right)=\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}$
392 382 391 oveq12d ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to \left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{t}\right)-{Y}}{{t}}\right)\left({s}\right)\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{t}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}\right)\left({s}\right)=\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
393 392 eqcomd ${⊢}\left(\left({\phi }\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to \left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)=\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{t}\right)-{Y}}{{t}}\right)\left({s}\right)\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{t}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}\right)\left({s}\right)$
394 393 adantllr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to \left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)=\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{t}\right)-{Y}}{{t}}\right)\left({s}\right)\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{t}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}\right)\left({s}\right)$
395 369 371 394 3eqtrd ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)\to {O}\left({s}\right)=\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{t}\right)-{Y}}{{t}}\right)\left({s}\right)\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{t}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}\right)\left({s}\right)$
396 395 mpteq2dva ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼{O}\left({s}\right)\right)=\left({s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{t}\right)-{Y}}{{t}}\right)\left({s}\right)\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{t}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}\right)\left({s}\right)\right)$
397 350 396 eqtr2d ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{t}\right)-{Y}}{{t}}\right)\left({s}\right)\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{t}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}\right)\left({s}\right)\right)={{O}↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}$
398 397 oveq2d ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \frac{d\left({s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{t}\right)-{Y}}{{t}}\right)\left({s}\right)\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{t}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}\right)\left({s}\right)\right)}{{d}_{ℝ}{s}}=ℝ\mathrm{D}\left({{O}↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}\right)$
399 66 a1i ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to ℝ\subseteq ℂ$
400 349 317 sstrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq ℝ$
401 49 tgioo2 ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
402 49 401 dvres ${⊢}\left(\left(ℝ\subseteq ℂ\wedge {O}:\left[{d},\mathrm{\pi }\right]⟶ℂ\right)\wedge \left(\left[{d},\mathrm{\pi }\right]\subseteq ℝ\wedge \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq ℝ\right)\right)\to ℝ\mathrm{D}\left({{O}↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}\right)={{{O}}_{ℝ}^{\prime }↾}_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)}$
403 399 311 317 400 402 syl22anc ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to ℝ\mathrm{D}\left({{O}↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}\right)={{{O}}_{ℝ}^{\prime }↾}_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)}$
404 ioontr ${⊢}\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)=\left({J}\left({k}\right),{J}\left({k}+1\right)\right)$
405 404 a1i ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)=\left({J}\left({k}\right),{J}\left({k}+1\right)\right)$
406 405 reseq2d ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {{{O}}_{ℝ}^{\prime }↾}_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\right)}={{{O}}_{ℝ}^{\prime }↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}$
407 398 403 406 3eqtrrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {{{O}}_{ℝ}^{\prime }↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}=\frac{d\left({s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{t}\right)-{Y}}{{t}}\right)\left({s}\right)\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{t}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}\right)\left({s}\right)\right)}{{d}_{ℝ}{s}}$
408 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {F}:ℝ⟶ℝ$
409 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {X}\in ℝ$
410 4 ad2antrr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {M}\in ℕ$
411 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {V}\in {P}\left({M}\right)$
412 9 ad4ant14 ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)\underset{cn}{⟶}ℝ$
413 85 adantr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left[{d},\mathrm{\pi }\right]\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
414 349 413 sstrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
415 76 a1i ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to 0\in {ℝ}^{*}$
416 0red ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to 0\in ℝ$
417 79 ad2antlr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to 0<{d}$
418 416 322 320 417 326 ltletrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to 0<{J}\left({k}\right)$
419 320 331 415 418 ltnelicc ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to ¬0\in \left[{J}\left({k}\right),{J}\left({k}+1\right)\right]$
420 54 ad2antrr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {Y}\in ℝ$
421 42 a1i ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \mathrm{\pi }\in ℝ$
422 281 adantr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {d}<\mathrm{\pi }$
423 simpr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {k}\in \left(0..^{N}\right)$
424 biid ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {i}\in \left(0..^{M}\right)\right)\wedge \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\wedge {v}\in \left(0..^{M}\right)\right)\wedge \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({v}\right),{Q}\left({v}+1\right)\right)\right)↔\left(\left(\left(\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {i}\in \left(0..^{M}\right)\right)\wedge \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\wedge {v}\in \left(0..^{M}\right)\right)\wedge \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({v}\right),{Q}\left({v}+1\right)\right)\right)$
425 409 3 410 411 322 421 422 413 29 26 27 28 423 298 424 fourierdlem50 ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left(\left(\iota {l}\in \left(0..^{M}\right)|\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({l}\right),{Q}\left({l}+1\right)\right)\right)\in \left(0..^{M}\right)\wedge \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left(\left(\iota {l}\in \left(0..^{M}\right)|\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({l}\right),{Q}\left({l}+1\right)\right)\right)\right),{Q}\left(\left(\iota {l}\in \left(0..^{M}\right)|\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({l}\right),{Q}\left({l}+1\right)\right)\right)+1\right)\right)\right)$
426 425 simpld ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left(\iota {l}\in \left(0..^{M}\right)|\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({l}\right),{Q}\left({l}+1\right)\right)\right)\in \left(0..^{M}\right)$
427 425 simprd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left(\left(\iota {l}\in \left(0..^{M}\right)|\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({l}\right),{Q}\left({l}+1\right)\right)\right)\right),{Q}\left(\left(\iota {l}\in \left(0..^{M}\right)|\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({l}\right),{Q}\left({l}+1\right)\right)\right)+1\right)\right)$
428 377 cbvmptv ${⊢}\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{t}\right)-{Y}}{{t}}\right)=\left({s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)$
429 387 cbvmptv ${⊢}\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{t}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}\right)=\left({s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
430 eqid ${⊢}\left({s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{t}\right)-{Y}}{{t}}\right)\left({s}\right)\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{t}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}\right)\left({s}\right)\right)=\left({s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{t}\right)-{Y}}{{t}}\right)\left({s}\right)\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{t}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}\right)\left({s}\right)\right)$
431 408 409 3 410 411 412 320 330 191 414 419 420 29 426 427 428 429 430 fourierdlem72 ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \frac{d\left({s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{t}\right)-{Y}}{{t}}\right)\left({s}\right)\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{t}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}\right)\left({s}\right)\right)}{{d}_{ℝ}{s}}:\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\underset{cn}{⟶}ℂ$
432 407 431 eqeltrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({{{O}}_{ℝ}^{\prime }↾}_{\left({J}\left({k}\right),{J}\left({k}+1\right)\right)}\right):\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\underset{cn}{⟶}ℂ$
433 eqid ${⊢}\left({s}\in \left[{d},\mathrm{\pi }\right]⟼\frac{{F}\left({X}+{s}\right)-{Y}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)=\left({s}\in \left[{d},\mathrm{\pi }\right]⟼\frac{{F}\left({X}+{s}\right)-{Y}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
434 eqid ${⊢}\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)=\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)$
435 30 426 eqeltrid ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {C}\in \left(0..^{M}\right)$
436 simpll ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {\phi }$
437 436 435 jca ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({\phi }\wedge {C}\in \left(0..^{M}\right)\right)$
438 eleq1 ${⊢}{i}={C}\to \left({i}\in \left(0..^{M}\right)↔{C}\in \left(0..^{M}\right)\right)$
439 438 anbi2d ${⊢}{i}={C}\to \left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)↔\left({\phi }\wedge {C}\in \left(0..^{M}\right)\right)\right)$
440 fveq2 ${⊢}{i}={C}\to {V}\left({i}\right)={V}\left({C}\right)$
441 oveq1 ${⊢}{i}={C}\to {i}+1={C}+1$
442 441 fveq2d ${⊢}{i}={C}\to {V}\left({i}+1\right)={V}\left({C}+1\right)$
443 440 442 oveq12d ${⊢}{i}={C}\to \left({V}\left({i}\right),{V}\left({i}+1\right)\right)=\left({V}\left({C}\right),{V}\left({C}+1\right)\right)$
444 raleq ${⊢}\left({V}\left({i}\right),{V}\left({i}+1\right)\right)=\left({V}\left({C}\right),{V}\left({C}+1\right)\right)\to \left(\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}↔\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\right)$
445 443 444 syl ${⊢}{i}={C}\to \left(\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}↔\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\right)$
446 445 rexbidv ${⊢}{i}={C}\to \left(\exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}↔\exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\right)$
447 439 446 imbi12d ${⊢}{i}={C}\to \left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\right)↔\left(\left({\phi }\wedge {C}\in \left(0..^{M}\right)\right)\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\right)\right)$
448 447 8 vtoclg ${⊢}{C}\in \left(0..^{M}\right)\to \left(\left({\phi }\wedge {C}\in \left(0..^{M}\right)\right)\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\right)$
449 435 437 448 sylc ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}$
450 nfv ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)$
451 nfra1 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}$
452 450 451 nfan ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\right)$
453 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to \forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}$
454 70 a1i ${⊢}{\phi }\to -\mathrm{\pi }\in ℝ$
455 454 2 readdcld ${⊢}{\phi }\to -\mathrm{\pi }+{X}\in ℝ$
456 42 a1i ${⊢}{\phi }\to \mathrm{\pi }\in ℝ$
457 456 2 readdcld ${⊢}{\phi }\to \mathrm{\pi }+{X}\in ℝ$
458 455 457 iccssred ${⊢}{\phi }\to \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]\subseteq ℝ$
459 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
460 458 459 sstrdi ${⊢}{\phi }\to \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]\subseteq {ℝ}^{*}$
461 460 ad2antrr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]\subseteq {ℝ}^{*}$
462 3 410 411 fourierdlem15 ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {V}:\left(0\dots {M}\right)⟶\left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]$
463 elfzofz ${⊢}{C}\in \left(0..^{M}\right)\to {C}\in \left(0\dots {M}\right)$
464 435 463 syl ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {C}\in \left(0\dots {M}\right)$
465 462 464 ffvelrnd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {V}\left({C}\right)\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]$
466 461 465 sseldd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {V}\left({C}\right)\in {ℝ}^{*}$
467 466 adantr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {V}\left({C}\right)\in {ℝ}^{*}$
468 fzofzp1 ${⊢}{C}\in \left(0..^{M}\right)\to {C}+1\in \left(0\dots {M}\right)$
469 435 468 syl ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {C}+1\in \left(0\dots {M}\right)$
470 462 469 ffvelrnd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {V}\left({C}+1\right)\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]$
471 461 470 sseldd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {V}\left({C}+1\right)\in {ℝ}^{*}$
472 471 adantr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {V}\left({C}+1\right)\in {ℝ}^{*}$
473 elioore ${⊢}{t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\to {t}\in ℝ$
474 473 adantl ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {t}\in ℝ$
475 70 a1i ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to -\mathrm{\pi }\in ℝ$
476 475 421 409 3 410 411 464 29 fourierdlem13 ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({Q}\left({C}\right)={V}\left({C}\right)-{X}\wedge {V}\left({C}\right)={X}+{Q}\left({C}\right)\right)$
477 476 simprd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {V}\left({C}\right)={X}+{Q}\left({C}\right)$
478 477 adantr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {V}\left({C}\right)={X}+{Q}\left({C}\right)$
479 458 ad2antrr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]\subseteq ℝ$
480 479 465 sseldd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {V}\left({C}\right)\in ℝ$
481 480 adantr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {V}\left({C}\right)\in ℝ$
482 478 481 eqeltrrd ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {X}+{Q}\left({C}\right)\in ℝ$
483 409 320 readdcld ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {X}+{J}\left({k}\right)\in ℝ$
484 483 adantr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {X}+{J}\left({k}\right)\in ℝ$
485 476 simpld ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {Q}\left({C}\right)={V}\left({C}\right)-{X}$
486 480 409 resubcld ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {V}\left({C}\right)-{X}\in ℝ$
487 485 486 eqeltrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {Q}\left({C}\right)\in ℝ$
488 475 421 409 3 410 411 469 29 fourierdlem13 ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({Q}\left({C}+1\right)={V}\left({C}+1\right)-{X}\wedge {V}\left({C}+1\right)={X}+{Q}\left({C}+1\right)\right)$
489 488 simpld ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {Q}\left({C}+1\right)={V}\left({C}+1\right)-{X}$
490 479 470 sseldd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {V}\left({C}+1\right)\in ℝ$
491 490 409 resubcld ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {V}\left({C}+1\right)-{X}\in ℝ$
492 489 491 eqeltrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {Q}\left({C}+1\right)\in ℝ$
493 30 eqcomi ${⊢}\left(\iota {l}\in \left(0..^{M}\right)|\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({l}\right),{Q}\left({l}+1\right)\right)\right)={C}$
494 493 fveq2i ${⊢}{Q}\left(\left(\iota {l}\in \left(0..^{M}\right)|\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({l}\right),{Q}\left({l}+1\right)\right)\right)\right)={Q}\left({C}\right)$
495 493 oveq1i ${⊢}\left(\iota {l}\in \left(0..^{M}\right)|\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({l}\right),{Q}\left({l}+1\right)\right)\right)+1={C}+1$
496 495 fveq2i ${⊢}{Q}\left(\left(\iota {l}\in \left(0..^{M}\right)|\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({l}\right),{Q}\left({l}+1\right)\right)\right)+1\right)={Q}\left({C}+1\right)$
497 494 496 oveq12i ${⊢}\left({Q}\left(\left(\iota {l}\in \left(0..^{M}\right)|\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({l}\right),{Q}\left({l}+1\right)\right)\right)\right),{Q}\left(\left(\iota {l}\in \left(0..^{M}\right)|\left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({l}\right),{Q}\left({l}+1\right)\right)\right)+1\right)\right)=\left({Q}\left({C}\right),{Q}\left({C}+1\right)\right)$
498 427 497 sseqtrdi ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({J}\left({k}\right),{J}\left({k}+1\right)\right)\subseteq \left({Q}\left({C}\right),{Q}\left({C}+1\right)\right)$
499 487 492 320 330 191 498 fourierdlem10 ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({Q}\left({C}\right)\le {J}\left({k}\right)\wedge {J}\left({k}+1\right)\le {Q}\left({C}+1\right)\right)$
500 499 simpld ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {Q}\left({C}\right)\le {J}\left({k}\right)$
501 487 320 409 500 leadd2dd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {X}+{Q}\left({C}\right)\le {X}+{J}\left({k}\right)$
502 501 adantr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {X}+{Q}\left({C}\right)\le {X}+{J}\left({k}\right)$
503 484 rexrd ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {X}+{J}\left({k}\right)\in {ℝ}^{*}$
504 409 330 readdcld ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {X}+{J}\left({k}+1\right)\in ℝ$
505 504 rexrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {X}+{J}\left({k}+1\right)\in {ℝ}^{*}$
506 505 adantr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {X}+{J}\left({k}+1\right)\in {ℝ}^{*}$
507 simpr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)$
508 ioogtlb ${⊢}\left({X}+{J}\left({k}\right)\in {ℝ}^{*}\wedge {X}+{J}\left({k}+1\right)\in {ℝ}^{*}\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {X}+{J}\left({k}\right)<{t}$
509 503 506 507 508 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {X}+{J}\left({k}\right)<{t}$
510 482 484 474 502 509 lelttrd ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {X}+{Q}\left({C}\right)<{t}$
511 478 510 eqbrtrd ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {V}\left({C}\right)<{t}$
512 504 adantr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {X}+{J}\left({k}+1\right)\in ℝ$
513 488 simprd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {V}\left({C}+1\right)={X}+{Q}\left({C}+1\right)$
514 513 490 eqeltrrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {X}+{Q}\left({C}+1\right)\in ℝ$
515 514 adantr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {X}+{Q}\left({C}+1\right)\in ℝ$
516 iooltub ${⊢}\left({X}+{J}\left({k}\right)\in {ℝ}^{*}\wedge {X}+{J}\left({k}+1\right)\in {ℝ}^{*}\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {t}<{X}+{J}\left({k}+1\right)$
517 503 506 507 516 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {t}<{X}+{J}\left({k}+1\right)$
518 499 simprd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {J}\left({k}+1\right)\le {Q}\left({C}+1\right)$
519 330 492 409 518 leadd2dd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {X}+{J}\left({k}+1\right)\le {X}+{Q}\left({C}+1\right)$
520 519 adantr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {X}+{J}\left({k}+1\right)\le {X}+{Q}\left({C}+1\right)$
521 474 512 515 517 520 ltletrd ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {t}<{X}+{Q}\left({C}+1\right)$
522 513 eqcomd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {X}+{Q}\left({C}+1\right)={V}\left({C}+1\right)$
523 522 adantr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {X}+{Q}\left({C}+1\right)={V}\left({C}+1\right)$
524 521 523 breqtrd ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {t}<{V}\left({C}+1\right)$
525 467 472 474 511 524 eliood ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)$
526 525 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)$
527 rspa ${⊢}\left(\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\wedge {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\right)\to \left|{F}\left({t}\right)\right|\le {w}$
528 453 526 527 syl2anc ${⊢}\left(\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to \left|{F}\left({t}\right)\right|\le {w}$
529 528 ex ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\right)\to \left({t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\to \left|{F}\left({t}\right)\right|\le {w}\right)$
530 452 529 ralrimi ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\right)\to \forall {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}$
531 530 ex ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left(\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\to \forall {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\right)$
532 531 reximdv ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left(\exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\right)$
533 449 532 mpd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}$
534 443 raleqdv ${⊢}{i}={C}\to \left(\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}↔\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)$
535 534 rexbidv ${⊢}{i}={C}\to \left(\exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}↔\exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)$
536 439 535 imbi12d ${⊢}{i}={C}\to \left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)↔\left(\left({\phi }\wedge {C}\in \left(0..^{M}\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)\right)$
537 536 10 vtoclg ${⊢}{C}\in \left(0..^{M}\right)\to \left(\left({\phi }\wedge {C}\in \left(0..^{M}\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)$
538 435 437 537 sylc ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
539 nfra1 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
540 450 539 nfan ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)$
541 1 67 fssd ${⊢}{\phi }\to {F}:ℝ⟶ℂ$
542 ssid ${⊢}ℝ\subseteq ℝ$
543 542 a1i ${⊢}{\phi }\to ℝ\subseteq ℝ$
544 ioossre ${⊢}\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\subseteq ℝ$
545 544 a1i ${⊢}{\phi }\to \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\subseteq ℝ$
546 49 401 dvres ${⊢}\left(\left(ℝ\subseteq ℂ\wedge {F}:ℝ⟶ℂ\right)\wedge \left(ℝ\subseteq ℝ\wedge \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\subseteq ℝ\right)\right)\to ℝ\mathrm{D}\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)={{{F}}_{ℝ}^{\prime }↾}_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)}$
547 67 541 543 545 546 syl22anc ${⊢}{\phi }\to ℝ\mathrm{D}\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)={{{F}}_{ℝ}^{\prime }↾}_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)}$
548 ioontr ${⊢}\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)=\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)$
549 548 reseq2i ${⊢}{{{F}}_{ℝ}^{\prime }↾}_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)}={{{F}}_{ℝ}^{\prime }↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}$
550 547 549 syl6eq ${⊢}{\phi }\to ℝ\mathrm{D}\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)={{{F}}_{ℝ}^{\prime }↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}$
551 550 fveq1d ${⊢}{\phi }\to {\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({t}\right)=\left({{{F}}_{ℝ}^{\prime }↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)\left({t}\right)$
552 fvres ${⊢}{t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)\left({t}\right)={{F}}_{ℝ}^{\prime }\left({t}\right)$
553 551 552 sylan9eq ${⊢}\left({\phi }\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({t}\right)={{F}}_{ℝ}^{\prime }\left({t}\right)$
554 553 ad4ant14 ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({t}\right)={{F}}_{ℝ}^{\prime }\left({t}\right)$
555 554 fveq2d ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to \left|{\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({t}\right)\right|=\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|$
556 555 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to \left|{\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({t}\right)\right|=\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|$
557 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to \forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
558 525 adantlr ${⊢}\left(\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)$
559 rspa ${⊢}\left(\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\wedge {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\right)\to \left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
560 557 558 559 syl2anc ${⊢}\left(\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to \left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
561 556 560 eqbrtrd ${⊢}\left(\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)\wedge {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)\to \left|{\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
562 561 ex ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)\to \left({t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\to \left|{\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)$
563 540 562 ralrimi ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)\to \forall {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
564 563 ex ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left(\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\to \forall {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)$
565 564 reximdv ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left(\exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)$
566 538 565 mpd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
567 323 324 318 423 fourierdlem8 ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left[{J}\left({k}\right),{J}\left({k}+1\right)\right]\subseteq \left[{d},\mathrm{\pi }\right]$
568 143 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {r}\in \left[{d},\mathrm{\pi }\right]\right)\wedge ¬{r}\in \mathrm{ran}{J}\right)\to {N}\in ℕ$
569 167 316 fssd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {J}:\left(0\dots {N}\right)⟶ℝ$
570 569 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {r}\in \left[{d},\mathrm{\pi }\right]\right)\wedge ¬{r}\in \mathrm{ran}{J}\right)\to {J}:\left(0\dots {N}\right)⟶ℝ$
571 simpr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {r}\in \left[{d},\mathrm{\pi }\right]\right)\to {r}\in \left[{d},\mathrm{\pi }\right]$
572 168 eqcomd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {d}={J}\left(0\right)$
573 169 eqcomd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \mathrm{\pi }={J}\left({N}\right)$
574 572 573 oveq12d ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \left[{d},\mathrm{\pi }\right]=\left[{J}\left(0\right),{J}\left({N}\right)\right]$
575 574 adantr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {r}\in \left[{d},\mathrm{\pi }\right]\right)\to \left[{d},\mathrm{\pi }\right]=\left[{J}\left(0\right),{J}\left({N}\right)\right]$
576 571 575 eleqtrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {r}\in \left[{d},\mathrm{\pi }\right]\right)\to {r}\in \left[{J}\left(0\right),{J}\left({N}\right)\right]$
577 576 adantr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {r}\in \left[{d},\mathrm{\pi }\right]\right)\wedge ¬{r}\in \mathrm{ran}{J}\right)\to {r}\in \left[{J}\left(0\right),{J}\left({N}\right)\right]$
578 simpr ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {r}\in \left[{d},\mathrm{\pi }\right]\right)\wedge ¬{r}\in \mathrm{ran}{J}\right)\to ¬{r}\in \mathrm{ran}{J}$
579 fveq2 ${⊢}{j}={k}\to {J}\left({j}\right)={J}\left({k}\right)$
580 579 breq1d ${⊢}{j}={k}\to \left({J}\left({j}\right)<{r}↔{J}\left({k}\right)<{r}\right)$
581 580 cbvrabv ${⊢}\left\{{j}\in \left(0..^{N}\right)|{J}\left({j}\right)<{r}\right\}=\left\{{k}\in \left(0..^{N}\right)|{J}\left({k}\right)<{r}\right\}$
582 581 supeq1i ${⊢}sup\left(\left\{{j}\in \left(0..^{N}\right)|{J}\left({j}\right)<{r}\right\},ℝ,<\right)=sup\left(\left\{{k}\in \left(0..^{N}\right)|{J}\left({k}\right)<{r}\right\},ℝ,<\right)$
583 568 570 577 578 582 fourierdlem25 ${⊢}\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {r}\in \left[{d},\mathrm{\pi }\right]\right)\wedge ¬{r}\in \mathrm{ran}{J}\right)\to \exists {m}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{r}\in \left({J}\left({m}\right),{J}\left({m}+1\right)\right)$
584 541 ad2antrr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {F}:ℝ⟶ℂ$
585 542 a1i ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to ℝ\subseteq ℝ$
586 544 a1i ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\subseteq ℝ$
587 399 584 585 586 546 syl22anc ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to ℝ\mathrm{D}\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)={{{F}}_{ℝ}^{\prime }↾}_{\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\right)}$
588 525 ralrimiva ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \forall {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}{t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)$
589 dfss3 ${⊢}\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\subseteq \left({V}\left({C}\right),{V}\left({C}+1\right)\right)↔\forall {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}{t}\in \left({V}\left({C}\right),{V}\left({C}+1\right)\right)$
590 588 589 sylibr ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\subseteq \left({V}\left({C}\right),{V}\left({C}+1\right)\right)$
591 resabs2 ${⊢}\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\subseteq \left({V}\left({C}\right),{V}\left({C}+1\right)\right)\to {\left({{{F}}_{ℝ}^{\prime }↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)↾}_{\left({V}\left({C}\right),{V}\left({C}+1\right)\right)}={{{F}}_{ℝ}^{\prime }↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}$
592 590 591 syl ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {\left({{{F}}_{ℝ}^{\prime }↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)↾}_{\left({V}\left({C}\right),{V}\left({C}+1\right)\right)}={{{F}}_{ℝ}^{\prime }↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}$
593 549 587 592 3eqtr4a ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to ℝ\mathrm{D}\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)={\left({{{F}}_{ℝ}^{\prime }↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)↾}_{\left({V}\left({C}\right),{V}\left({C}+1\right)\right)}$
594 590 resabs1d ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({C}\right),{V}\left({C}+1\right)\right)}\right)↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}={{{F}}_{ℝ}^{\prime }↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}$
595 594 eqcomd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {{{F}}_{ℝ}^{\prime }↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}={\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({C}\right),{V}\left({C}+1\right)\right)}\right)↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}$
596 593 592 595 3eqtrrd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({C}\right),{V}\left({C}+1\right)\right)}\right)↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}=ℝ\mathrm{D}\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)$
597 443 reseq2d ${⊢}{i}={C}\to {{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}={{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({C}\right),{V}\left({C}+1\right)\right)}$
598 597 443 feq12d ${⊢}{i}={C}\to \left(\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)⟶ℝ↔\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({C}\right),{V}\left({C}+1\right)\right)}\right):\left({V}\left({C}\right),{V}\left({C}+1\right)\right)⟶ℝ\right)$
599 439 598 imbi12d ${⊢}{i}={C}\to \left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)⟶ℝ\right)↔\left(\left({\phi }\wedge {C}\in \left(0..^{M}\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({C}\right),{V}\left({C}+1\right)\right)}\right):\left({V}\left({C}\right),{V}\left({C}+1\right)\right)⟶ℝ\right)\right)$
600 cncff ${⊢}\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)\underset{cn}{⟶}ℝ\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)⟶ℝ$
601 9 600 syl ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)⟶ℝ$
602 599 601 vtoclg ${⊢}{C}\in \left(0..^{M}\right)\to \left(\left({\phi }\wedge {C}\in \left(0..^{M}\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({C}\right),{V}\left({C}+1\right)\right)}\right):\left({V}\left({C}\right),{V}\left({C}+1\right)\right)⟶ℝ\right)$
603 602 anabsi7 ${⊢}\left({\phi }\wedge {C}\in \left(0..^{M}\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({C}\right),{V}\left({C}+1\right)\right)}\right):\left({V}\left({C}\right),{V}\left({C}+1\right)\right)⟶ℝ$
604 437 603 syl ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({C}\right),{V}\left({C}+1\right)\right)}\right):\left({V}\left({C}\right),{V}\left({C}+1\right)\right)⟶ℝ$
605 604 590 fssresd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to \left({\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({C}\right),{V}\left({C}+1\right)\right)}\right)↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right):\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)⟶ℝ$
606 596 605 feq1dd ${⊢}\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\to {\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }:\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)⟶ℝ$
607 375 386 oveq12d ${⊢}{t}={s}\to \frac{{F}\left({X}+{t}\right)-{Y}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}=\frac{{F}\left({X}+{s}\right)-{Y}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}$
608 607 cbvmptv ${⊢}\left({t}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{t}\right)-{Y}}{2\mathrm{sin}\left(\frac{{t}}{2}\right)}\right)=\left({s}\in \left({J}\left({k}\right),{J}\left({k}+1\right)\right)⟼\frac{{F}\left({X}+{s}\right)-{Y}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
609 fveq2 ${⊢}{r}={t}\to {F}\left({r}\right)={F}\left({t}\right)$
610 609 fveq2d ${⊢}{r}={t}\to \left|{F}\left({r}\right)\right|=\left|{F}\left({t}\right)\right|$
611 610 breq1d ${⊢}{r}={t}\to \left(\left|{F}\left({r}\right)\right|\le {w}↔\left|{F}\left({t}\right)\right|\le {w}\right)$
612 611 cbvralvw ${⊢}\forall {r}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({r}\right)\right|\le {w}↔\forall {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}$
613 612 anbi2i ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {w}\in ℝ\right)\wedge {z}\in ℝ\right)\wedge \forall {r}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({r}\right)\right|\le {w}\right)↔\left(\left(\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {w}\in ℝ\right)\wedge {z}\in ℝ\right)\wedge \forall {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\right)$
614 fveq2 ${⊢}{r}={t}\to {\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({r}\right)={\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({t}\right)$
615 614 fveq2d ${⊢}{r}={t}\to \left|{\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({r}\right)\right|=\left|{\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({t}\right)\right|$
616 615 breq1d ${⊢}{r}={t}\to \left(\left|{\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({r}\right)\right|\le {z}↔\left|{\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)$
617 616 cbvralvw ${⊢}\forall {r}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({r}\right)\right|\le {z}↔\forall {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
618 613 617 anbi12i ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {w}\in ℝ\right)\wedge {z}\in ℝ\right)\wedge \forall {r}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({r}\right)\right|\le {w}\right)\wedge \forall {r}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({r}\right)\right|\le {z}\right)↔\left(\left(\left(\left(\left(\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\wedge {k}\in \left(0..^{N}\right)\right)\wedge {w}\in ℝ\right)\wedge {z}\in ℝ\right)\wedge \forall {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\right)\wedge \forall {t}\in \left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|{\left({{F}↾}_{\left({X}+{J}\left({k}\right),{X}+{J}\left({k}+1\right)\right)}\right)}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)$
619 274 275 41 43 85 288 289 433 434 533 566 167 191 567 583 606 608 618 fourierdlem80 ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \exists {b}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {s}\in \mathrm{dom}\frac{d\left({s}\in \left[{d},\mathrm{\pi }\right]⟼\frac{{F}\left({X}+{s}\right)-{Y}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)}{{d}_{ℝ}{s}}\phantom{\rule{.4em}{0ex}}\left|\frac{d\left({s}\in \left[{d},\mathrm{\pi }\right]⟼\frac{{F}\left({X}+{s}\right)-{Y}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)}{{d}_{ℝ}{s}}\left({s}\right)\right|\le {b}$
620 366 mpteq2dva ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to \left({s}\in \left[{d},\mathrm{\pi }\right]⟼\left(\frac{{F}\left({X}+{s}\right)-{Y}}{{s}}\right)\left(\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)=\left({s}\in \left[{d},\mathrm{\pi }\right]⟼\frac{{F}\left({X}+{s}\right)-{Y}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
621 271 620 eqtrd ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to {O}=\left({s}\in \left[{d},\mathrm{\pi }\right]⟼\frac{{F}\left({X}+{s}\right)-{Y}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
622 621 oveq2d ${⊢}\left({\phi }\wedge {d}\in \left(0,\mathrm{\pi }\right)\right)\to ℝ\mathrm{D}{O}=\frac{d\left({s}\in \left[{d},\mathrm{\pi }\right]⟼\frac{{F}\left({X}+{s}\right)-{Y}}{2\mathrm{sin}&ApplyFunctio}\right)}{}$