# Metamath Proof Explorer

## Theorem fourierdlem112

Description: Here abbreviations (local definitions) are introduced to prove the fourier theorem. ( Zm ) is the m_th partial sum of the fourier series. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem112.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
fourierdlem112.d ${⊢}{D}=\left({m}\in ℕ⟼\left({y}\in ℝ⟼if\left({y}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{m}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({m}+\left(\frac{1}{2}\right)\right){y}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{y}}{2}\right)}\right)\right)\right)$
fourierdlem112.p ${⊢}{P}=\left({n}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {n}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }\wedge {p}\left({n}\right)=\mathrm{\pi }\right)\wedge \forall {i}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}\right)$
fourierdlem112.m ${⊢}{\phi }\to {M}\in ℕ$
fourierdlem112.q ${⊢}{\phi }\to {Q}\in {P}\left({M}\right)$
fourierdlem112.n ${⊢}{N}=\left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1$
fourierdlem112.v ${⊢}{V}=\left(\iota {f}|{f}{Isom}_{<,<}\left(\left(0\dots {N}\right),\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right)\right)$
fourierdlem112.x ${⊢}{\phi }\to {X}\in ℝ$
fourierdlem112.xran ${⊢}{\phi }\to {X}\in \mathrm{ran}{V}$
fourierdlem112.t ${⊢}{T}=2\mathrm{\pi }$
fourierdlem112.fper ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)$
fourierdlem112.fcn ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right):\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
fourierdlem112.c ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {C}\in \left(\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)\right)$
fourierdlem112.u ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {U}\in \left(\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)\right)$
fourierdlem112.fdvcn ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right):\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
fourierdlem112.e ${⊢}{\phi }\to {E}\in \left(\left({{{F}}_{ℝ}^{\prime }↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
fourierdlem112.i ${⊢}{\phi }\to {I}\in \left(\left({{{F}}_{ℝ}^{\prime }↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
fourierdlem112.l ${⊢}{\phi }\to {L}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
fourierdlem112.r ${⊢}{\phi }\to {R}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
fourierdlem112.a ${⊢}{A}=\left({n}\in {ℕ}_{0}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{n}{x}d{x}}{\mathrm{\pi }}\right)$
fourierdlem112.b ${⊢}{B}=\left({n}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{n}{x}d{x}}{\mathrm{\pi }}\right)$
fourierdlem112.z ${⊢}{Z}=\left({m}\in ℕ⟼\left(\frac{{A}\left(0\right)}{2}\right)+\sum _{{n}=1}^{{m}}\left({A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)\right)$
fourierdlem112.23 ${⊢}{S}=\left({n}\in ℕ⟼{A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)$
fourierdlem112.fbd ${⊢}{\phi }\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in ℝ\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}$
fourierdlem112.fdvbd ${⊢}{\phi }\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
fourierdlem112.25 ${⊢}{\phi }\to {X}\in ℝ$
Assertion fourierdlem112 ${⊢}{\phi }\to \left(seq1\left(+,{S}\right)⇝\left(\left(\frac{{L}+{R}}{2}\right)-\left(\frac{{A}\left(0\right)}{2}\right)\right)\wedge \left(\frac{{A}\left(0\right)}{2}\right)+\sum _{{n}\in ℕ}\left({A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)=\frac{{L}+{R}}{2}\right)$

### Proof

Step Hyp Ref Expression
1 fourierdlem112.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
2 fourierdlem112.d ${⊢}{D}=\left({m}\in ℕ⟼\left({y}\in ℝ⟼if\left({y}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{m}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({m}+\left(\frac{1}{2}\right)\right){y}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{y}}{2}\right)}\right)\right)\right)$
3 fourierdlem112.p ${⊢}{P}=\left({n}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {n}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }\wedge {p}\left({n}\right)=\mathrm{\pi }\right)\wedge \forall {i}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}\right)$
4 fourierdlem112.m ${⊢}{\phi }\to {M}\in ℕ$
5 fourierdlem112.q ${⊢}{\phi }\to {Q}\in {P}\left({M}\right)$
6 fourierdlem112.n ${⊢}{N}=\left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1$
7 fourierdlem112.v ${⊢}{V}=\left(\iota {f}|{f}{Isom}_{<,<}\left(\left(0\dots {N}\right),\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right)\right)$
8 fourierdlem112.x ${⊢}{\phi }\to {X}\in ℝ$
9 fourierdlem112.xran ${⊢}{\phi }\to {X}\in \mathrm{ran}{V}$
10 fourierdlem112.t ${⊢}{T}=2\mathrm{\pi }$
11 fourierdlem112.fper ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)$
12 fourierdlem112.fcn ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right):\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
13 fourierdlem112.c ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {C}\in \left(\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)\right)$
14 fourierdlem112.u ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {U}\in \left(\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)\right)$
15 fourierdlem112.fdvcn ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right):\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
16 fourierdlem112.e ${⊢}{\phi }\to {E}\in \left(\left({{{F}}_{ℝ}^{\prime }↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
17 fourierdlem112.i ${⊢}{\phi }\to {I}\in \left(\left({{{F}}_{ℝ}^{\prime }↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
18 fourierdlem112.l ${⊢}{\phi }\to {L}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
19 fourierdlem112.r ${⊢}{\phi }\to {R}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
20 fourierdlem112.a ${⊢}{A}=\left({n}\in {ℕ}_{0}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{n}{x}d{x}}{\mathrm{\pi }}\right)$
21 fourierdlem112.b ${⊢}{B}=\left({n}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{n}{x}d{x}}{\mathrm{\pi }}\right)$
22 fourierdlem112.z ${⊢}{Z}=\left({m}\in ℕ⟼\left(\frac{{A}\left(0\right)}{2}\right)+\sum _{{n}=1}^{{m}}\left({A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)\right)$
23 fourierdlem112.23 ${⊢}{S}=\left({n}\in ℕ⟼{A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)$
24 fourierdlem112.fbd ${⊢}{\phi }\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in ℝ\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}$
25 fourierdlem112.fdvbd ${⊢}{\phi }\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
26 fourierdlem112.25 ${⊢}{\phi }\to {X}\in ℝ$
27 fveq2 ${⊢}{n}={j}\to {A}\left({n}\right)={A}\left({j}\right)$
28 oveq1 ${⊢}{n}={j}\to {n}{X}={j}{X}$
29 28 fveq2d ${⊢}{n}={j}\to \mathrm{cos}{n}{X}=\mathrm{cos}{j}{X}$
30 27 29 oveq12d ${⊢}{n}={j}\to {A}\left({n}\right)\mathrm{cos}{n}{X}={A}\left({j}\right)\mathrm{cos}{j}{X}$
31 fveq2 ${⊢}{n}={j}\to {B}\left({n}\right)={B}\left({j}\right)$
32 28 fveq2d ${⊢}{n}={j}\to \mathrm{sin}{n}{X}=\mathrm{sin}{j}{X}$
33 31 32 oveq12d ${⊢}{n}={j}\to {B}\left({n}\right)\mathrm{sin}{n}{X}={B}\left({j}\right)\mathrm{sin}{j}{X}$
34 30 33 oveq12d ${⊢}{n}={j}\to {A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}={A}\left({j}\right)\mathrm{cos}{j}{X}+{B}\left({j}\right)\mathrm{sin}{j}{X}$
35 34 cbvmptv ${⊢}\left({n}\in ℕ⟼{A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)=\left({j}\in ℕ⟼{A}\left({j}\right)\mathrm{cos}{j}{X}+{B}\left({j}\right)\mathrm{sin}{j}{X}\right)$
36 23 35 eqtri ${⊢}{S}=\left({j}\in ℕ⟼{A}\left({j}\right)\mathrm{cos}{j}{X}+{B}\left({j}\right)\mathrm{sin}{j}{X}\right)$
37 seqeq3 ${⊢}{S}=\left({j}\in ℕ⟼{A}\left({j}\right)\mathrm{cos}{j}{X}+{B}\left({j}\right)\mathrm{sin}{j}{X}\right)\to seq1\left(+,{S}\right)=seq1\left(+,\left({j}\in ℕ⟼{A}\left({j}\right)\mathrm{cos}{j}{X}+{B}\left({j}\right)\mathrm{sin}{j}{X}\right)\right)$
38 36 37 mp1i ${⊢}{\phi }\to seq1\left(+,{S}\right)=seq1\left(+,\left({j}\in ℕ⟼{A}\left({j}\right)\mathrm{cos}{j}{X}+{B}\left({j}\right)\mathrm{sin}{j}{X}\right)\right)$
39 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
40 1zzd ${⊢}{\phi }\to 1\in ℤ$
41 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{\phi }$
42 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}ℕ$
43 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left(-\mathrm{\pi },0\right)$
44 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{F}\left({X}+{s}\right)$
45 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}×$
46 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{D}\left({m}\right)\left({s}\right)$
47 44 45 46 nfov ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)$
48 43 47 nfitg ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}$
49 42 48 nfmpt ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({m}\in ℕ⟼{\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}\right)$
50 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left(0,\mathrm{\pi }\right)$
51 50 47 nfitg ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}$
52 42 51 nfmpt ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({m}\in ℕ⟼{\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}\right)$
53 nfmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in {ℕ}_{0}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{n}{x}d{x}}{\mathrm{\pi }}\right)$
54 20 53 nfcxfr ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{A}$
55 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}0$
56 54 55 nffv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{A}\left(0\right)$
57 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}÷$
58 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}2$
59 56 57 58 nfov ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left(\frac{{A}\left(0\right)}{2}\right)$
60 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}+$
61 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left(1\dots {m}\right)$
62 61 nfsum1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\sum _{{n}=1}^{{m}}\left({A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)$
63 59 60 62 nfov ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left(\left(\frac{{A}\left(0\right)}{2}\right)+\sum _{{n}=1}^{{m}}\left({A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)\right)$
64 42 63 nfmpt ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({m}\in ℕ⟼\left(\frac{{A}\left(0\right)}{2}\right)+\sum _{{n}=1}^{{m}}\left({A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)\right)$
65 22 64 nfcxfr ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{Z}$
66 eqid ${⊢}\left({n}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {n}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }+{X}\wedge {p}\left({n}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}\right)=\left({n}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {n}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }+{X}\wedge {p}\left({n}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}\right)$
67 picn ${⊢}\mathrm{\pi }\in ℂ$
68 67 2timesi ${⊢}2\mathrm{\pi }=\mathrm{\pi }+\mathrm{\pi }$
69 67 67 subnegi ${⊢}\mathrm{\pi }-\left(-\mathrm{\pi }\right)=\mathrm{\pi }+\mathrm{\pi }$
70 68 10 69 3eqtr4i ${⊢}{T}=\mathrm{\pi }-\left(-\mathrm{\pi }\right)$
71 pire ${⊢}\mathrm{\pi }\in ℝ$
72 71 a1i ${⊢}{\phi }\to \mathrm{\pi }\in ℝ$
73 72 renegcld ${⊢}{\phi }\to -\mathrm{\pi }\in ℝ$
74 73 26 readdcld ${⊢}{\phi }\to -\mathrm{\pi }+{X}\in ℝ$
75 72 26 readdcld ${⊢}{\phi }\to \mathrm{\pi }+{X}\in ℝ$
76 negpilt0 ${⊢}-\mathrm{\pi }<0$
77 pipos ${⊢}0<\mathrm{\pi }$
78 71 renegcli ${⊢}-\mathrm{\pi }\in ℝ$
79 0re ${⊢}0\in ℝ$
80 78 79 71 lttri ${⊢}\left(-\mathrm{\pi }<0\wedge 0<\mathrm{\pi }\right)\to -\mathrm{\pi }<\mathrm{\pi }$
81 76 77 80 mp2an ${⊢}-\mathrm{\pi }<\mathrm{\pi }$
82 81 a1i ${⊢}{\phi }\to -\mathrm{\pi }<\mathrm{\pi }$
83 73 72 26 82 ltadd1dd ${⊢}{\phi }\to -\mathrm{\pi }+{X}<\mathrm{\pi }+{X}$
84 oveq1 ${⊢}{y}={x}\to {y}+{k}{T}={x}+{k}{T}$
85 84 eleq1d ${⊢}{y}={x}\to \left({y}+{k}{T}\in \mathrm{ran}{Q}↔{x}+{k}{T}\in \mathrm{ran}{Q}\right)$
86 85 rexbidv ${⊢}{y}={x}\to \left(\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}↔\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{x}+{k}{T}\in \mathrm{ran}{Q}\right)$
87 86 cbvrabv ${⊢}\left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}=\left\{{x}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{x}+{k}{T}\in \mathrm{ran}{Q}\right\}$
88 87 uneq2i ${⊢}\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}=\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{x}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{x}+{k}{T}\in \mathrm{ran}{Q}\right\}$
89 70 3 4 5 74 75 83 66 88 6 7 fourierdlem54 ${⊢}{\phi }\to \left(\left({N}\in ℕ\wedge {V}\in \left({n}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {n}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }+{X}\wedge {p}\left({n}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}\right)\left({N}\right)\right)\wedge {V}{Isom}_{<,<}\left(\left(0\dots {N}\right),\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right)\right)$
90 89 simpld ${⊢}{\phi }\to \left({N}\in ℕ\wedge {V}\in \left({n}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {n}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }+{X}\wedge {p}\left({n}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}\right)\left({N}\right)\right)$
91 90 simpld ${⊢}{\phi }\to {N}\in ℕ$
92 90 simprd ${⊢}{\phi }\to {V}\in \left({n}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {n}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }+{X}\wedge {p}\left({n}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}\right)\left({N}\right)$
93 1 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to {F}:ℝ⟶ℝ$
94 fveq2 ${⊢}{i}={j}\to {p}\left({i}\right)={p}\left({j}\right)$
95 oveq1 ${⊢}{i}={j}\to {i}+1={j}+1$
96 95 fveq2d ${⊢}{i}={j}\to {p}\left({i}+1\right)={p}\left({j}+1\right)$
97 94 96 breq12d ${⊢}{i}={j}\to \left({p}\left({i}\right)<{p}\left({i}+1\right)↔{p}\left({j}\right)<{p}\left({j}+1\right)\right)$
98 97 cbvralvw ${⊢}\forall {i}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)↔\forall {j}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({j}\right)<{p}\left({j}+1\right)$
99 98 anbi2i ${⊢}\left(\left({p}\left(0\right)=-\mathrm{\pi }\wedge {p}\left({n}\right)=\mathrm{\pi }\right)\wedge \forall {i}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)↔\left(\left({p}\left(0\right)=-\mathrm{\pi }\wedge {p}\left({n}\right)=\mathrm{\pi }\right)\wedge \forall {j}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({j}\right)<{p}\left({j}+1\right)\right)$
100 99 a1i ${⊢}{p}\in \left({ℝ}^{\left(0\dots {n}\right)}\right)\to \left(\left(\left({p}\left(0\right)=-\mathrm{\pi }\wedge {p}\left({n}\right)=\mathrm{\pi }\right)\wedge \forall {i}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)↔\left(\left({p}\left(0\right)=-\mathrm{\pi }\wedge {p}\left({n}\right)=\mathrm{\pi }\right)\wedge \forall {j}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({j}\right)<{p}\left({j}+1\right)\right)\right)$
101 100 rabbiia ${⊢}\left\{{p}\in \left({ℝ}^{\left(0\dots {n}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }\wedge {p}\left({n}\right)=\mathrm{\pi }\right)\wedge \forall {i}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}=\left\{{p}\in \left({ℝ}^{\left(0\dots {n}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }\wedge {p}\left({n}\right)=\mathrm{\pi }\right)\wedge \forall {j}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({j}\right)<{p}\left({j}+1\right)\right)\right\}$
102 101 mpteq2i ${⊢}\left({n}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {n}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }\wedge {p}\left({n}\right)=\mathrm{\pi }\right)\wedge \forall {i}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}\right)=\left({n}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {n}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }\wedge {p}\left({n}\right)=\mathrm{\pi }\right)\wedge \forall {j}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({j}\right)<{p}\left({j}+1\right)\right)\right\}\right)$
103 3 102 eqtri ${⊢}{P}=\left({n}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {n}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }\wedge {p}\left({n}\right)=\mathrm{\pi }\right)\wedge \forall {j}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({j}\right)<{p}\left({j}+1\right)\right)\right\}\right)$
104 4 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to {M}\in ℕ$
105 5 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to {Q}\in {P}\left({M}\right)$
106 11 adantlr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\wedge {x}\in ℝ\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)$
107 eleq1w ${⊢}{i}={j}\to \left({i}\in \left(0..^{M}\right)↔{j}\in \left(0..^{M}\right)\right)$
108 107 anbi2d ${⊢}{i}={j}\to \left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)↔\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\right)$
109 fveq2 ${⊢}{i}={j}\to {Q}\left({i}\right)={Q}\left({j}\right)$
110 95 fveq2d ${⊢}{i}={j}\to {Q}\left({i}+1\right)={Q}\left({j}+1\right)$
111 109 110 oveq12d ${⊢}{i}={j}\to \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)=\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)$
112 111 reseq2d ${⊢}{i}={j}\to {{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}={{F}↾}_{\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)}$
113 111 oveq1d
114 112 113 eleq12d ${⊢}{i}={j}\to \left(\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right):\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ↔\left({{F}↾}_{\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)}\right):\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)\underset{cn}{⟶}ℂ\right)$
115 108 114 imbi12d ${⊢}{i}={j}\to \left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right):\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ\right)↔\left(\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to \left({{F}↾}_{\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)}\right):\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)\underset{cn}{⟶}ℂ\right)\right)$
116 115 12 chvarvv ${⊢}\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to \left({{F}↾}_{\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)}\right):\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)\underset{cn}{⟶}ℂ$
117 116 adantlr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\wedge {j}\in \left(0..^{M}\right)\right)\to \left({{F}↾}_{\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)}\right):\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)\underset{cn}{⟶}ℂ$
118 74 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to -\mathrm{\pi }+{X}\in ℝ$
119 74 rexrd ${⊢}{\phi }\to -\mathrm{\pi }+{X}\in {ℝ}^{*}$
120 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
121 120 a1i ${⊢}{\phi }\to \mathrm{+\infty }\in {ℝ}^{*}$
122 75 ltpnfd ${⊢}{\phi }\to \mathrm{\pi }+{X}<\mathrm{+\infty }$
123 119 121 75 83 122 eliood ${⊢}{\phi }\to \mathrm{\pi }+{X}\in \left(-\mathrm{\pi }+{X},\mathrm{+\infty }\right)$
124 123 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to \mathrm{\pi }+{X}\in \left(-\mathrm{\pi }+{X},\mathrm{+\infty }\right)$
125 id ${⊢}{i}\in \left(0..^{N}\right)\to {i}\in \left(0..^{N}\right)$
126 6 oveq2i ${⊢}\left(0..^{N}\right)=\left(0..^\left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1\right)$
127 125 126 eleqtrdi ${⊢}{i}\in \left(0..^{N}\right)\to {i}\in \left(0..^\left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1\right)$
128 127 adantl ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to {i}\in \left(0..^\left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1\right)$
129 6 oveq2i ${⊢}\left(0\dots {N}\right)=\left(0\dots \left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1\right)$
130 isoeq4 ${⊢}\left(0\dots {N}\right)=\left(0\dots \left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1\right)\to \left({f}{Isom}_{<,<}\left(\left(0\dots {N}\right),\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right)↔{f}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1\right),\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right)\right)$
131 129 130 ax-mp ${⊢}{f}{Isom}_{<,<}\left(\left(0\dots {N}\right),\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right)↔{f}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1\right),\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right)$
132 131 iotabii ${⊢}\left(\iota {f}|{f}{Isom}_{<,<}\left(\left(0\dots {N}\right),\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right)\right)=\left(\iota {f}|{f}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1\right),\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right)\right)$
133 7 132 eqtri ${⊢}{V}=\left(\iota {f}|{f}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1\right),\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right)\right)$
134 93 103 70 104 105 106 117 118 124 128 133 fourierdlem98 ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\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}{⟶}ℂ$
135 24 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to \exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in ℝ\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}$
136 nfra1 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\forall {t}\in ℝ\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}$
137 elioore ${⊢}{t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\to {t}\in ℝ$
138 rspa ${⊢}\left(\forall {t}\in ℝ\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\wedge {t}\in ℝ\right)\to \left|{F}\left({t}\right)\right|\le {w}$
139 137 138 sylan2 ${⊢}\left(\forall {t}\in ℝ\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\wedge {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\right)\to \left|{F}\left({t}\right)\right|\le {w}$
140 139 ex ${⊢}\forall {t}\in ℝ\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\to \left({t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\to \left|{F}\left({t}\right)\right|\le {w}\right)$
141 136 140 ralrimi ${⊢}\forall {t}\in ℝ\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\to \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}$
142 141 reximi ${⊢}\exists {w}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in ℝ\phantom{\rule{.4em}{0ex}}\left|{F}\left({t}\right)\right|\le {w}\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}$
143 135 142 syl ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\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}$
144 ssid ${⊢}ℝ\subseteq ℝ$
145 dvfre ${⊢}\left({F}:ℝ⟶ℝ\wedge ℝ\subseteq ℝ\right)\to {{F}}_{ℝ}^{\prime }:\mathrm{dom}{{F}}_{ℝ}^{\prime }⟶ℝ$
146 1 144 145 sylancl ${⊢}{\phi }\to {{F}}_{ℝ}^{\prime }:\mathrm{dom}{{F}}_{ℝ}^{\prime }⟶ℝ$
147 146 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to {{F}}_{ℝ}^{\prime }:\mathrm{dom}{{F}}_{ℝ}^{\prime }⟶ℝ$
148 eqid ${⊢}ℝ\mathrm{D}{F}=ℝ\mathrm{D}{F}$
149 71 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to \mathrm{\pi }\in ℝ$
150 78 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to -\mathrm{\pi }\in ℝ$
151 111 reseq2d ${⊢}{i}={j}\to {{{F}}_{ℝ}^{\prime }↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}={{{F}}_{ℝ}^{\prime }↾}_{\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)}$
152 151 113 eleq12d ${⊢}{i}={j}\to \left(\left({{{F}}_{ℝ}^{\prime }↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right):\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ↔\left({{{F}}_{ℝ}^{\prime }↾}_{\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)}\right):\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)\underset{cn}{⟶}ℂ\right)$
153 108 152 imbi12d ${⊢}{i}={j}\to \left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right):\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ\right)↔\left(\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)}\right):\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)\underset{cn}{⟶}ℂ\right)\right)$
154 153 15 chvarvv ${⊢}\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)}\right):\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)\underset{cn}{⟶}ℂ$
155 154 adantlr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\wedge {j}\in \left(0..^{M}\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)}\right):\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)\underset{cn}{⟶}ℂ$
156 73 8 readdcld ${⊢}{\phi }\to -\mathrm{\pi }+{X}\in ℝ$
157 156 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to -\mathrm{\pi }+{X}\in ℝ$
158 156 rexrd ${⊢}{\phi }\to -\mathrm{\pi }+{X}\in {ℝ}^{*}$
159 72 8 readdcld ${⊢}{\phi }\to \mathrm{\pi }+{X}\in ℝ$
160 73 72 8 82 ltadd1dd ${⊢}{\phi }\to -\mathrm{\pi }+{X}<\mathrm{\pi }+{X}$
161 159 ltpnfd ${⊢}{\phi }\to \mathrm{\pi }+{X}<\mathrm{+\infty }$
162 158 121 159 160 161 eliood ${⊢}{\phi }\to \mathrm{\pi }+{X}\in \left(-\mathrm{\pi }+{X},\mathrm{+\infty }\right)$
163 162 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to \mathrm{\pi }+{X}\in \left(-\mathrm{\pi }+{X},\mathrm{+\infty }\right)$
164 oveq1 ${⊢}{k}={h}\to {k}{T}={h}{T}$
165 164 oveq2d ${⊢}{k}={h}\to {y}+{k}{T}={y}+{h}{T}$
166 165 eleq1d ${⊢}{k}={h}\to \left({y}+{k}{T}\in \mathrm{ran}{Q}↔{y}+{h}{T}\in \mathrm{ran}{Q}\right)$
167 166 cbvrexvw ${⊢}\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}↔\exists {h}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{h}{T}\in \mathrm{ran}{Q}$
168 167 rgenw ${⊢}\forall {y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]\phantom{\rule{.4em}{0ex}}\left(\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}↔\exists {h}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{h}{T}\in \mathrm{ran}{Q}\right)$
169 rabbi ${⊢}\forall {y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]\phantom{\rule{.4em}{0ex}}\left(\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}↔\exists {h}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{h}{T}\in \mathrm{ran}{Q}\right)↔\left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}=\left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {h}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{h}{T}\in \mathrm{ran}{Q}\right\}$
170 168 169 mpbi ${⊢}\left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}=\left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {h}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{h}{T}\in \mathrm{ran}{Q}\right\}$
171 170 uneq2i ${⊢}\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}=\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {h}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{h}{T}\in \mathrm{ran}{Q}\right\}$
172 isoeq5 ${⊢}\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}=\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {h}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{h}{T}\in \mathrm{ran}{Q}\right\}\to \left({f}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1\right),\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right)↔{f}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1\right),\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {h}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{h}{T}\in \mathrm{ran}{Q}\right\}\right)\right)$
173 171 172 ax-mp ${⊢}{f}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1\right),\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right)↔{f}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1\right),\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {h}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{h}{T}\in \mathrm{ran}{Q}\right\}\right)$
174 173 iotabii ${⊢}\left(\iota {f}|{f}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1\right),\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right)\right)=\left(\iota {f}|{f}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1\right),\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {h}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{h}{T}\in \mathrm{ran}{Q}\right\}\right)\right)$
175 133 174 eqtri ${⊢}{V}=\left(\iota {f}|{f}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{k}{T}\in \mathrm{ran}{Q}\right\}\right|-1\right),\left\{-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right\}\cup \left\{{y}\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]|\exists {h}\in ℤ\phantom{\rule{.4em}{0ex}}{y}+{h}{T}\in \mathrm{ran}{Q}\right\}\right)\right)$
176 eleq1w ${⊢}{v}={u}\to \left({v}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }↔{u}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)$
177 fveq2 ${⊢}{v}={u}\to {{F}}_{ℝ}^{\prime }\left({v}\right)={{F}}_{ℝ}^{\prime }\left({u}\right)$
178 176 177 ifbieq1d ${⊢}{v}={u}\to if\left({v}\in \mathrm{dom}{{F}}_{ℝ}^{\prime },{{F}}_{ℝ}^{\prime }\left({v}\right),0\right)=if\left({u}\in \mathrm{dom}{{F}}_{ℝ}^{\prime },{{F}}_{ℝ}^{\prime }\left({u}\right),0\right)$
179 178 cbvmptv ${⊢}\left({v}\in ℝ⟼if\left({v}\in \mathrm{dom}{{F}}_{ℝ}^{\prime },{{F}}_{ℝ}^{\prime }\left({v}\right),0\right)\right)=\left({u}\in ℝ⟼if\left({u}\in \mathrm{dom}{{F}}_{ℝ}^{\prime },{{F}}_{ℝ}^{\prime }\left({u}\right),0\right)\right)$
180 93 148 103 149 150 70 104 105 106 155 157 163 128 175 179 fourierdlem97 ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\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}{⟶}ℂ$
181 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)⟶ℂ$
182 fdm ${⊢}\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)⟶ℂ\to \mathrm{dom}\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)$
183 180 181 182 3syl ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to \mathrm{dom}\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)$
184 ssdmres ${⊢}\left({V}\left({i}\right),{V}\left({i}+1\right)\right)\subseteq \mathrm{dom}{{F}}_{ℝ}^{\prime }↔\mathrm{dom}\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)$
185 183 184 sylibr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\subseteq \mathrm{dom}{{F}}_{ℝ}^{\prime }$
186 147 185 fssresd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\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)⟶ℝ$
187 ax-resscn ${⊢}ℝ\subseteq ℂ$
188 187 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to ℝ\subseteq ℂ$
189 cncffvrn ${⊢}\left(ℝ\subseteq ℂ\wedge \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}{⟶}ℂ\right)\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)\underset{cn}{⟶}ℝ↔\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)$
190 188 180 189 syl2anc ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\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)\underset{cn}{⟶}ℝ↔\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)$
191 186 190 mpbird ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\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}{⟶}ℝ$
192 25 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to \exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
193 nfv ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)$
194 nfra1 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\forall {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
195 193 194 nfan ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)$
196 fvres ${⊢}{t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)={{F}}_{ℝ}^{\prime }\left({t}\right)$
197 196 adantl ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\right)\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)={{F}}_{ℝ}^{\prime }\left({t}\right)$
198 197 fveq2d ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\right)\to \left|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|=\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|$
199 198 adantlr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)\wedge {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\right)\to \left|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|=\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|$
200 simplr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)\wedge {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\right)\to \forall {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
201 185 sselda ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\wedge {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\right)\to {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }$
202 201 adantlr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)\wedge {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\right)\to {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }$
203 rspa ${⊢}\left(\forall {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\wedge {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\right)\to \left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
204 200 202 203 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)\wedge {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\right)\to \left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
205 199 204 eqbrtrd ${⊢}\left(\left(\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)\wedge {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\right)\to \left|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|\le {z}$
206 205 ex ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)\to \left({t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\to \left|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|\le {z}\right)$
207 195 206 ralrimi ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\wedge \forall {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)\to \forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|\le {z}$
208 207 ex ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to \left(\forall {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\phantom{\rule{.4em}{0ex}}\left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\to \forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|\le {z}\right)$
209 208 reximdv ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to \left(\exists {z}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {t}\in \mathrm{dom}{{F}}_{ℝ}^{\prime }\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({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|\le {z}\right)$
210 192 209 mpd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\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|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|\le {z}$
211 nfra1 ${⊢}Ⅎ{t}\phantom{\rule{.4em}{0ex}}\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|\le {z}$
212 196 eqcomd ${⊢}{t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\to {{F}}_{ℝ}^{\prime }\left({t}\right)=\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)$
213 212 fveq2d ${⊢}{t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\to \left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|=\left|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|$
214 213 adantl ${⊢}\left(\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|\le {z}\wedge {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\right)\to \left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|=\left|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|$
215 rspa ${⊢}\left(\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|\le {z}\wedge {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\right)\to \left|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|\le {z}$
216 214 215 eqbrtrd ${⊢}\left(\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|\le {z}\wedge {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\right)\to \left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}$
217 216 ex ${⊢}\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|\le {z}\to \left({t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\to \left|{{F}}_{ℝ}^{\prime }\left({t}\right)\right|\le {z}\right)$
218 211 217 ralrimi ${⊢}\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|\le {z}\to \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}$
219 218 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\to \left(\forall {t}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|\le {z}\to \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)$
220 219 reximdv ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\right)\right)\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|\left({{{F}}_{ℝ}^{\prime }↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right)\left({t}\right)\right|\le {z}\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)$
221 210 220 mpd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{N}\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}$
222 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {j}\in \left(0..^{M}\right)\right)$
223 nfcsb1v
224 223 nfel1
225 222 224 nfim
226 csbeq1a
227 112 109 oveq12d ${⊢}{i}={j}\to \left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)=\left({{F}↾}_{\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({j}\right)$
228 226 227 eleq12d
229 108 228 imbi12d
230 225 229 13 chvarfv
232 93 103 70 104 105 106 117 231 118 124 128 133 fourierdlem96
233 nfcsb1v
234 233 nfel1
235 222 234 nfim
236 csbeq1a
237 112 110 oveq12d ${⊢}{i}={j}\to \left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)=\left({{F}↾}_{\left({Q}\left({j}\right),{Q}\left({j}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({j}+1\right)$
238 236 237 eleq12d
239 108 238 imbi12d
240 235 239 14 chvarfv
242 93 103 70 104 105 106 117 241 157 163 128 133 fourierdlem99
243 eqeq1 ${⊢}{g}={s}\to \left({g}=0↔{s}=0\right)$
244 oveq2 ${⊢}{g}={s}\to {X}+{g}={X}+{s}$
245 244 fveq2d ${⊢}{g}={s}\to {F}\left({X}+{g}\right)={F}\left({X}+{s}\right)$
246 breq2 ${⊢}{g}={s}\to \left(0<{g}↔0<{s}\right)$
247 246 ifbid ${⊢}{g}={s}\to if\left(0<{g},{R},{L}\right)=if\left(0<{s},{R},{L}\right)$
248 245 247 oveq12d ${⊢}{g}={s}\to {F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)={F}\left({X}+{s}\right)-if\left(0<{s},{R},{L}\right)$
249 id ${⊢}{g}={s}\to {g}={s}$
250 248 249 oveq12d ${⊢}{g}={s}\to \frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}=\frac{{F}\left({X}+{s}\right)-if\left(0<{s},{R},{L}\right)}{{s}}$
251 243 250 ifbieq2d ${⊢}{g}={s}\to if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)=if\left({s}=0,0,\frac{{F}\left({X}+{s}\right)-if\left(0<{s},{R},{L}\right)}{{s}}\right)$
252 251 cbvmptv ${⊢}\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({s}=0,0,\frac{{F}\left({X}+{s}\right)-if\left(0<{s},{R},{L}\right)}{{s}}\right)\right)$
253 eqeq1 ${⊢}{o}={s}\to \left({o}=0↔{s}=0\right)$
254 id ${⊢}{o}={s}\to {o}={s}$
255 oveq1 ${⊢}{o}={s}\to \frac{{o}}{2}=\frac{{s}}{2}$
256 255 fveq2d ${⊢}{o}={s}\to \mathrm{sin}\left(\frac{{o}}{2}\right)=\mathrm{sin}\left(\frac{{s}}{2}\right)$
257 256 oveq2d ${⊢}{o}={s}\to 2\mathrm{sin}\left(\frac{{o}}{2}\right)=2\mathrm{sin}\left(\frac{{s}}{2}\right)$
258 254 257 oveq12d ${⊢}{o}={s}\to \frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}=\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}$
259 253 258 ifbieq2d ${⊢}{o}={s}\to if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)=if\left({s}=0,1,\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
260 259 cbvmptv ${⊢}\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)=\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)$
261 fveq2 ${⊢}{r}={s}\to \left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)=\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({s}\right)$
262 fveq2 ${⊢}{r}={s}\to \left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)=\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({s}\right)$
263 261 262 oveq12d ${⊢}{r}={s}\to \left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)=\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({s}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({s}\right)$
264 263 cbvmptv ${⊢}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({s}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({s}\right)\right)$
265 oveq2 ${⊢}{d}={s}\to \left({k}+\left(\frac{1}{2}\right)\right){d}=\left({k}+\left(\frac{1}{2}\right)\right){s}$
266 265 fveq2d ${⊢}{d}={s}\to \mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}=\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}$
267 266 cbvmptv ${⊢}\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}\right)$
268 fveq2 ${⊢}{z}={s}\to \left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)=\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)$
269 fveq2 ${⊢}{z}={s}\to \left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)=\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({s}\right)$
270 268 269 oveq12d ${⊢}{z}={s}\to \left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)=\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({s}\right)$
271 270 cbvmptv ${⊢}\left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({s}\right)\right)$
272 fveq2 ${⊢}{m}={n}\to {D}\left({m}\right)={D}\left({n}\right)$
273 272 fveq1d ${⊢}{m}={n}\to {D}\left({m}\right)\left({s}\right)={D}\left({n}\right)\left({s}\right)$
274 273 oveq2d ${⊢}{m}={n}\to {F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)={F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)$
275 274 adantr ${⊢}\left({m}={n}\wedge {s}\in \left(-\mathrm{\pi },0\right)\right)\to {F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)={F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)$
276 275 itgeq2dv ${⊢}{m}={n}\to {\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}={\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}$
277 276 cbvmptv ${⊢}\left({m}\in ℕ⟼{\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}\right)=\left({n}\in ℕ⟼{\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}\right)$
278 oveq1 ${⊢}{c}={k}\to {c}+\left(\frac{1}{2}\right)={k}+\left(\frac{1}{2}\right)$
279 278 oveq1d ${⊢}{c}={k}\to \left({c}+\left(\frac{1}{2}\right)\right){d}=\left({k}+\left(\frac{1}{2}\right)\right){d}$
280 279 fveq2d ${⊢}{c}={k}\to \mathrm{sin}\left({c}+\left(\frac{1}{2}\right)\right){d}=\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}$
281 280 mpteq2dv ${⊢}{c}={k}\to \left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({c}+\left(\frac{1}{2}\right)\right){d}\right)=\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)$
282 281 fveq1d ${⊢}{c}={k}\to \left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({c}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)=\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)$
283 282 oveq2d ${⊢}{c}={k}\to \left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({c}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)=\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)$
284 283 mpteq2dv ${⊢}{c}={k}\to \left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({c}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)=\left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)$
285 284 fveq1d ${⊢}{c}={k}\to \left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({c}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)=\left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)$
286 285 adantr ${⊢}\left({c}={k}\wedge {s}\in \left(-\mathrm{\pi },0\right)\right)\to \left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({c}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)=\left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)$
287 286 itgeq2dv ${⊢}{c}={k}\to {\int }_{\left(-\mathrm{\pi },0\right)}\left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({c}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)d{s}={\int }_{\left(-\mathrm{\pi },0\right)}\left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)d{s}$
288 287 oveq1d ${⊢}{c}={k}\to \frac{{\int }_{\left(-\mathrm{\pi },0\right)}\left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({c}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)d{s}}{\mathrm{\pi }}=\frac{{\int }_{\left(-\mathrm{\pi },0\right)}\left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)d{s}}{\mathrm{\pi }}$
289 288 cbvmptv ${⊢}\left({c}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },0\right)}\left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({c}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)d{s}}{\mathrm{\pi }}\right)=\left({k}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },0\right)}\left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)d{s}}{\mathrm{\pi }}\right)$
290 oveq1 ${⊢}{y}={s}\to {y}\mathrm{mod}2\mathrm{\pi }={s}\mathrm{mod}2\mathrm{\pi }$
291 290 eqeq1d ${⊢}{y}={s}\to \left({y}\mathrm{mod}2\mathrm{\pi }=0↔{s}\mathrm{mod}2\mathrm{\pi }=0\right)$
292 oveq2 ${⊢}{y}={s}\to \left({m}+\left(\frac{1}{2}\right)\right){y}=\left({m}+\left(\frac{1}{2}\right)\right){s}$
293 292 fveq2d ${⊢}{y}={s}\to \mathrm{sin}\left({m}+\left(\frac{1}{2}\right)\right){y}=\mathrm{sin}\left({m}+\left(\frac{1}{2}\right)\right){s}$
294 oveq1 ${⊢}{y}={s}\to \frac{{y}}{2}=\frac{{s}}{2}$
295 294 fveq2d ${⊢}{y}={s}\to \mathrm{sin}\left(\frac{{y}}{2}\right)=\mathrm{sin}\left(\frac{{s}}{2}\right)$
296 295 oveq2d ${⊢}{y}={s}\to 2\mathrm{\pi }\mathrm{sin}\left(\frac{{y}}{2}\right)=2\mathrm{\pi }\mathrm{sin}\left(\frac{{s}}{2}\right)$
297 293 296 oveq12d ${⊢}{y}={s}\to \frac{\mathrm{sin}\left({m}+\left(\frac{1}{2}\right)\right){y}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{y}}{2}\right)}=\frac{\mathrm{sin}\left({m}+\left(\frac{1}{2}\right)\right){s}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{s}}{2}\right)}$
298 291 297 ifbieq2d ${⊢}{y}={s}\to if\left({y}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{m}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({m}+\left(\frac{1}{2}\right)\right){y}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{y}}{2}\right)}\right)=if\left({s}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{m}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({m}+\left(\frac{1}{2}\right)\right){s}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
299 298 cbvmptv ${⊢}\left({y}\in ℝ⟼if\left({y}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{m}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({m}+\left(\frac{1}{2}\right)\right){y}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{y}}{2}\right)}\right)\right)=\left({s}\in ℝ⟼if\left({s}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{m}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({m}+\left(\frac{1}{2}\right)\right){s}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)$
300 simpl ${⊢}\left({m}={k}\wedge {s}\in ℝ\right)\to {m}={k}$
301 300 oveq2d ${⊢}\left({m}={k}\wedge {s}\in ℝ\right)\to 2{m}=2{k}$
302 301 oveq1d ${⊢}\left({m}={k}\wedge {s}\in ℝ\right)\to 2{m}+1=2{k}+1$
303 302 oveq1d ${⊢}\left({m}={k}\wedge {s}\in ℝ\right)\to \frac{2{m}+1}{2\mathrm{\pi }}=\frac{2{k}+1}{2\mathrm{\pi }}$
304 300 oveq1d ${⊢}\left({m}={k}\wedge {s}\in ℝ\right)\to {m}+\left(\frac{1}{2}\right)={k}+\left(\frac{1}{2}\right)$
305 304 oveq1d ${⊢}\left({m}={k}\wedge {s}\in ℝ\right)\to \left({m}+\left(\frac{1}{2}\right)\right){s}=\left({k}+\left(\frac{1}{2}\right)\right){s}$
306 305 fveq2d ${⊢}\left({m}={k}\wedge {s}\in ℝ\right)\to \mathrm{sin}\left({m}+\left(\frac{1}{2}\right)\right){s}=\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}$
307 306 oveq1d ${⊢}\left({m}={k}\wedge {s}\in ℝ\right)\to \frac{\mathrm{sin}\left({m}+\left(\frac{1}{2}\right)\right){s}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{s}}{2}\right)}=\frac{\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{s}}{2}\right)}$
308 303 307 ifeq12d ${⊢}\left({m}={k}\wedge {s}\in ℝ\right)\to if\left({s}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{m}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({m}+\left(\frac{1}{2}\right)\right){s}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)=if\left({s}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{k}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)$
309 308 mpteq2dva ${⊢}{m}={k}\to \left({s}\in ℝ⟼if\left({s}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{m}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({m}+\left(\frac{1}{2}\right)\right){s}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)=\left({s}\in ℝ⟼if\left({s}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{k}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)$
310 299 309 syl5eq ${⊢}{m}={k}\to \left({y}\in ℝ⟼if\left({y}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{m}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({m}+\left(\frac{1}{2}\right)\right){y}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{y}}{2}\right)}\right)\right)=\left({s}\in ℝ⟼if\left({s}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{k}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)$
311 310 cbvmptv ${⊢}\left({m}\in ℕ⟼\left({y}\in ℝ⟼if\left({y}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{m}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({m}+\left(\frac{1}{2}\right)\right){y}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{y}}{2}\right)}\right)\right)\right)=\left({k}\in ℕ⟼\left({s}\in ℝ⟼if\left({s}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{k}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)\right)$
312 2 311 eqtri ${⊢}{D}=\left({k}\in ℕ⟼\left({s}\in ℝ⟼if\left({s}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{k}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){s}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)\right)$
313 eqid ${⊢}{\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)↾}_{\left[-\mathrm{\pi },{l}\right]}={\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)↾}_{\left[-\mathrm{\pi },{l}\right]}$
314 eqid ${⊢}\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)=\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)$
315 eqid ${⊢}\left|\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right|-1=\left|\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right|-1$
316 isoeq1 ${⊢}{u}={w}\to \left({u}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right|-1\right),\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right)↔{w}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right|-1\right),\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right)\right)$
317 316 cbviotavw ${⊢}\left(\iota {u}|{u}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right|-1\right),\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right)\right)=\left(\iota {w}|{w}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right|-1\right),\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right)\right)$
318 fveq2 ${⊢}{j}={i}\to {V}\left({j}\right)={V}\left({i}\right)$
319 318 oveq1d ${⊢}{j}={i}\to {V}\left({j}\right)-{X}={V}\left({i}\right)-{X}$
320 319 cbvmptv ${⊢}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)=\left({i}\in \left(0\dots {N}\right)⟼{V}\left({i}\right)-{X}\right)$
321 eqid ${⊢}\left(\iota {m}\in \left(0..^{N}\right)|\left(\left(\iota {u}|{u}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right|-1\right),\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right)\right)\left({b}\right),\left(\iota {u}|{u}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right|-1\right),\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right)\right)\left({b}+1\right)\right)\subseteq \left(\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\left({m}\right),\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\left({m}+1\right)\right)\right)=\left(\iota {m}\in \left(0..^{N}\right)|\left(\left(\iota {u}|{u}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right|-1\right),\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right)\right)\left({b}\right),\left(\iota {u}|{u}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right|-1\right),\left\{-\mathrm{\pi },{l}\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left(-\mathrm{\pi },{l}\right)\right)\right)\right)\left({b}+1\right)\right)\subseteq \left(\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\left({m}\right),\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\left({m}+1\right)\right)\right)$
322 fveq2 ${⊢}{a}={s}\to \left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)=\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)$
323 oveq2 ${⊢}{a}={s}\to \left({b}+\left(\frac{1}{2}\right)\right){a}=\left({b}+\left(\frac{1}{2}\right)\right){s}$
324 323 fveq2d ${⊢}{a}={s}\to \mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}=\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}$
325 322 324 oveq12d ${⊢}{a}={s}\to \left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}=\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}$
326 325 cbvitgv ${⊢}{\int }_{\left({l},0\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}={\int }_{\left({l},0\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}$
327 326 fveq2i ${⊢}\left|{\int }_{\left({l},0\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}\right|=\left|{\int }_{\left({l},0\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}\right|$
328 327 breq1i ${⊢}\left|{\int }_{\left({l},0\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}\right|<\frac{{i}}{2}↔\left|{\int }_{\left({l},0\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{i}}{2}$
329 328 anbi2i ${⊢}\left(\left(\left(\left({\phi }\wedge {i}\in {ℝ}^{+}\right)\wedge {l}\in \left(-\mathrm{\pi },0\right)\right)\wedge {b}\in ℕ\right)\wedge \left|{\int }_{\left({l},0\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}\right|<\frac{{i}}{2}\right)↔\left(\left(\left(\left({\phi }\wedge {i}\in {ℝ}^{+}\right)\wedge {l}\in \left(-\mathrm{\pi },0\right)\right)\wedge {b}\in ℕ\right)\wedge \left|{\int }_{\left({l},0\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{i}}{2}\right)$
330 325 cbvitgv ${⊢}{\int }_{\left(-\mathrm{\pi },{l}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}={\int }_{\left(-\mathrm{\pi },{l}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}$
331 330 fveq2i ${⊢}\left|{\int }_{\left(-\mathrm{\pi },{l}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}\right|=\left|{\int }_{\left(-\mathrm{\pi },{l}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}\right|$
332 331 breq1i ${⊢}\left|{\int }_{\left(-\mathrm{\pi },{l}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}\right|<\frac{{i}}{2}↔\left|{\int }_{\left(-\mathrm{\pi },{l}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{i}}{2}$
333 329 332 anbi12i ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {i}\in {ℝ}^{+}\right)\wedge {l}\in \left(-\mathrm{\pi },0\right)\right)\wedge {b}\in ℕ\right)\wedge \left|{\int }_{\left({l},0\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}\right|<\frac{{i}}{2}\right)\wedge \left|{\int }_{\left(-\mathrm{\pi },{l}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}\right|<\frac{{i}}{2}\right)↔\left(\left(\left(\left(\left({\phi }\wedge {i}\in {ℝ}^{+}\right)\wedge {l}\in \left(-\mathrm{\pi },0\right)\right)\wedge {b}\in ℕ\right)\wedge \left|{\int }_{\left({l},0\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{i}}{2}\right)\wedge \left|{\int }_{\left(-\mathrm{\pi },{l}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{i}}{2}\right)$
334 1 26 66 91 92 9 134 143 191 221 232 242 252 260 264 267 271 277 289 19 18 16 17 312 313 314 315 317 320 321 333 fourierdlem103 ${⊢}{\phi }\to \left({m}\in ℕ⟼{\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}\right)⇝\left(\frac{{L}}{2}\right)$
335 nnex ${⊢}ℕ\in \mathrm{V}$
336 335 mptex ${⊢}\left({m}\in ℕ⟼\left(\frac{{A}\left(0\right)}{2}\right)+\sum _{{n}=1}^{{m}}\left({A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)\right)\in \mathrm{V}$
337 22 336 eqeltri ${⊢}{Z}\in \mathrm{V}$
338 337 a1i ${⊢}{\phi }\to {Z}\in \mathrm{V}$
339 274 adantr ${⊢}\left({m}={n}\wedge {s}\in \left(0,\mathrm{\pi }\right)\right)\to {F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)={F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)$
340 339 itgeq2dv ${⊢}{m}={n}\to {\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}={\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}$
341 340 cbvmptv ${⊢}\left({m}\in ℕ⟼{\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}\right)=\left({n}\in ℕ⟼{\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}\right)$
342 285 adantr ${⊢}\left({c}={k}\wedge {s}\in \left(0,\mathrm{\pi }\right)\right)\to \left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({c}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)=\left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)$
343 342 itgeq2dv ${⊢}{c}={k}\to {\int }_{\left(0,\mathrm{\pi }\right)}\left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({c}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)d{s}={\int }_{\left(0,\mathrm{\pi }\right)}\left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)d{s}$
344 343 oveq1d ${⊢}{c}={k}\to \frac{{\int }_{\left(0,\mathrm{\pi }\right)}\left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({c}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)d{s}}{\mathrm{\pi }}=\frac{{\int }_{\left(0,\mathrm{\pi }\right)}\left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)d{s}}{\mathrm{\pi }}$
345 344 cbvmptv ${⊢}\left({c}\in ℕ⟼\frac{{\int }_{\left(0,\mathrm{\pi }\right)}\left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({c}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)d{s}}{\mathrm{\pi }}\right)=\left({k}\in ℕ⟼\frac{{\int }_{\left(0,\mathrm{\pi }\right)}\left({z}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({z}\right)\left({d}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({k}+\left(\frac{1}{2}\right)\right){d}\right)\left({z}\right)\right)\left({s}\right)d{s}}{\mathrm{\pi }}\right)$
346 eqid ${⊢}{\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)↾}_{\left[{e},\mathrm{\pi }\right]}={\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)↾}_{\left[{e},\mathrm{\pi }\right]}$
347 eqid ${⊢}\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)=\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)$
348 eqid ${⊢}\left|\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right|-1=\left|\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right|-1$
349 isoeq1 ${⊢}{u}={v}\to \left({u}{Isom}_{<,<}\left(\left(0\dots \left|\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right|-1\right),\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right)↔{v}{Isom}_{<,<}\left(\left(0\dots \left|\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right|-1\right),\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right)\right)$
350 349 cbviotavw ${⊢}\left(\iota {u}|{u}{Isom}_{<,<}\left(\left(0\dots \left|\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right|-1\right),\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right)\right)=\left(\iota {v}|{v}{Isom}_{<,<}\left(\left(0\dots \left|\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right|-1\right),\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right)\right)$
351 eqid ${⊢}\left(\iota {a}\in \left(0..^{N}\right)|\left(\left(\iota {u}|{u}{Isom}_{<,<}\left(\left(0\dots \left|\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right|-1\right),\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right)\right)\left({b}\right),\left(\iota {u}|{u}{Isom}_{<,<}\left(\left(0\dots \left|\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right|-1\right),\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right)\right)\left({b}+1\right)\right)\subseteq \left(\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\left({a}\right),\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\left({a}+1\right)\right)\right)=\left(\iota {a}\in \left(0..^{N}\right)|\left(\left(\iota {u}|{u}{Isom}_{<,<}\left(\left(0\dots \left|\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right|-1\right),\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right)\right)\left({b}\right),\left(\iota {u}|{u}{Isom}_{<,<}\left(\left(0\dots \left|\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right|-1\right),\left\{{e},\mathrm{\pi }\right\}\cup \left(\mathrm{ran}\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\cap \left({e},\mathrm{\pi }\right)\right)\right)\right)\left({b}+1\right)\right)\subseteq \left(\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\left({a}\right),\left({j}\in \left(0\dots {N}\right)⟼{V}\left({j}\right)-{X}\right)\left({a}+1\right)\right)\right)$
352 325 cbvitgv ${⊢}{\int }_{\left(0,{e}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}={\int }_{\left(0,{e}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}$
353 352 fveq2i ${⊢}\left|{\int }_{\left(0,{e}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}\right|=\left|{\int }_{\left(0,{e}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}\right|$
354 353 breq1i ${⊢}\left|{\int }_{\left(0,{e}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}\right|<\frac{{q}}{2}↔\left|{\int }_{\left(0,{e}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{q}}{2}$
355 354 anbi2i ${⊢}\left(\left(\left(\left({\phi }\wedge {q}\in {ℝ}^{+}\right)\wedge {e}\in \left(0,\mathrm{\pi }\right)\right)\wedge {b}\in ℕ\right)\wedge \left|{\int }_{\left(0,{e}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}\right|<\frac{{q}}{2}\right)↔\left(\left(\left(\left({\phi }\wedge {q}\in {ℝ}^{+}\right)\wedge {e}\in \left(0,\mathrm{\pi }\right)\right)\wedge {b}\in ℕ\right)\wedge \left|{\int }_{\left(0,{e}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{q}}{2}\right)$
356 325 cbvitgv ${⊢}{\int }_{\left({e},\mathrm{\pi }\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}={\int }_{\left({e},\mathrm{\pi }\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}$
357 356 fveq2i ${⊢}\left|{\int }_{\left({e},\mathrm{\pi }\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}\right|=\left|{\int }_{\left({e},\mathrm{\pi }\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}\right|$
358 357 breq1i ${⊢}\left|{\int }_{\left({e},\mathrm{\pi }\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}\right|<\frac{{q}}{2}↔\left|{\int }_{\left({e},\mathrm{\pi }\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{q}}{2}$
359 355 358 anbi12i ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {q}\in {ℝ}^{+}\right)\wedge {e}\in \left(0,\mathrm{\pi }\right)\right)\wedge {b}\in ℕ\right)\wedge \left|{\int }_{\left(0,{e}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}\right|<\frac{{q}}{2}\right)\wedge \left|{\int }_{\left({e},\mathrm{\pi }\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({a}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){a}d{a}\right|<\frac{{q}}{2}\right)↔\left(\left(\left(\left(\left({\phi }\wedge {q}\in {ℝ}^{+}\right)\wedge {e}\in \left(0,\mathrm{\pi }\right)\right)\wedge {b}\in ℕ\right)\wedge \left|{\int }_{\left(0,{e}\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{q}}{2}\right)\wedge \left|{\int }_{\left({e},\mathrm{\pi }\right)}\left({r}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({g}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({g}=0,0,\frac{{F}\left({X}+{g}\right)-if\left(0<{g},{R},{L}\right)}{{g}}\right)\right)\left({r}\right)\left({o}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({o}=0,1,\frac{{o}}{2\mathrm{sin}\left(\frac{{o}}{2}\right)}\right)\right)\left({r}\right)\right)\left({s}\right)\mathrm{sin}\left({b}+\left(\frac{1}{2}\right)\right){s}d{s}\right|<\frac{{q}}{2}\right)$
360 1 26 66 91 92 9 134 143 191 221 232 242 252 260 264 267 271 341 345 19 18 16 17 312 346 347 348 350 320 351 359 fourierdlem104 ${⊢}{\phi }\to \left({m}\in ℕ⟼{\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}\right)⇝\left(\frac{{R}}{2}\right)$
361 eqidd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({m}\in ℕ⟼{\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}\right)=\left({m}\in ℕ⟼{\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}\right)$
362 276 adantl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {m}={n}\right)\to {\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}={\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}$
363 simpr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}\in ℕ$
364 elioore ${⊢}{s}\in \left(-\mathrm{\pi },0\right)\to {s}\in ℝ$
365 1 adantr ${⊢}\left({\phi }\wedge {s}\in ℝ\right)\to {F}:ℝ⟶ℝ$
366 26 adantr ${⊢}\left({\phi }\wedge {s}\in ℝ\right)\to {X}\in ℝ$
367 simpr ${⊢}\left({\phi }\wedge {s}\in ℝ\right)\to {s}\in ℝ$
368 366 367 readdcld ${⊢}\left({\phi }\wedge {s}\in ℝ\right)\to {X}+{s}\in ℝ$
369 365 368 ffvelrnd ${⊢}\left({\phi }\wedge {s}\in ℝ\right)\to {F}\left({X}+{s}\right)\in ℝ$
370 369 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in ℝ\right)\to {F}\left({X}+{s}\right)\in ℝ$
371 2 dirkerre ${⊢}\left({n}\in ℕ\wedge {s}\in ℝ\right)\to {D}\left({n}\right)\left({s}\right)\in ℝ$
372 371 adantll ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in ℝ\right)\to {D}\left({n}\right)\left({s}\right)\in ℝ$
373 370 372 remulcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in ℝ\right)\to {F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\in ℝ$
374 364 373 sylan2 ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left(-\mathrm{\pi },0\right)\right)\to {F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\in ℝ$
375 ioossicc ${⊢}\left(-\mathrm{\pi },0\right)\subseteq \left[-\mathrm{\pi },0\right]$
376 78 leidi ${⊢}-\mathrm{\pi }\le -\mathrm{\pi }$
377 79 71 77 ltleii ${⊢}0\le \mathrm{\pi }$
378 iccss ${⊢}\left(\left(-\mathrm{\pi }\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\wedge \left(-\mathrm{\pi }\le -\mathrm{\pi }\wedge 0\le \mathrm{\pi }\right)\right)\to \left[-\mathrm{\pi },0\right]\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
379 78 71 376 377 378 mp4an ${⊢}\left[-\mathrm{\pi },0\right]\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
380 375 379 sstri ${⊢}\left(-\mathrm{\pi },0\right)\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
381 380 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(-\mathrm{\pi },0\right)\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
382 ioombl ${⊢}\left(-\mathrm{\pi },0\right)\in \mathrm{dom}vol$
383 382 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(-\mathrm{\pi },0\right)\in \mathrm{dom}vol$
384 1 adantr ${⊢}\left({\phi }\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {F}:ℝ⟶ℝ$
385 26 adantr ${⊢}\left({\phi }\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {X}\in ℝ$
386 73 72 iccssred ${⊢}{\phi }\to \left[-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℝ$
387 386 sselda ${⊢}\left({\phi }\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {s}\in ℝ$
388 385 387 readdcld ${⊢}\left({\phi }\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {X}+{s}\in ℝ$
389 384 388 ffvelrnd ${⊢}\left({\phi }\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {F}\left({X}+{s}\right)\in ℝ$
390 389 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {F}\left({X}+{s}\right)\in ℝ$
391 iccssre ${⊢}\left(-\mathrm{\pi }\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \left[-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℝ$
392 78 71 391 mp2an ${⊢}\left[-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℝ$
393 392 sseli ${⊢}{s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\to {s}\in ℝ$
394 393 371 sylan2 ${⊢}\left({n}\in ℕ\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {D}\left({n}\right)\left({s}\right)\in ℝ$
395 394 adantll ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {D}\left({n}\right)\left({s}\right)\in ℝ$
396 390 395 remulcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\in ℝ$
397 78 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to -\mathrm{\pi }\in ℝ$
398 71 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \mathrm{\pi }\in ℝ$
399 1 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {F}:ℝ⟶ℝ$
400 26 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {X}\in ℝ$
401 91 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {N}\in ℕ$
402 92 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {V}\in \left({n}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {n}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }+{X}\wedge {p}\left({n}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{n}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}\right)\left({N}\right)$
403 134 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{N}\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}{⟶}ℂ$
406 2 dirkercncf ${⊢}{n}\in ℕ\to {D}\left({n}\right):ℝ\underset{cn}{⟶}ℝ$
407 406 adantl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {D}\left({n}\right):ℝ\underset{cn}{⟶}ℝ$
408 eqid ${⊢}\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\right)=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\right)$
409 397 398 399 400 66 401 402 403 404 405 320 3 407 408 fourierdlem84 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\right)\in {𝐿}^{1}$
410 381 383 396 409 iblss ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({s}\in \left(-\mathrm{\pi },0\right)⟼{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\right)\in {𝐿}^{1}$
411 374 410 itgcl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}\in ℂ$
412 361 362 363 411 fvmptd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({m}\in ℕ⟼{\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}\right)\left({n}\right)={\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}$
413 412 411 eqeltrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({m}\in ℕ⟼{\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}\right)\left({n}\right)\in ℂ$
414 eqidd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({m}\in ℕ⟼{\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}\right)=\left({m}\in ℕ⟼{\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}\right)$
415 340 adantl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {m}={n}\right)\to {\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}={\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}$
416 1 adantr ${⊢}\left({\phi }\wedge {s}\in \left(0,\mathrm{\pi }\right)\right)\to {F}:ℝ⟶ℝ$
417 26 adantr ${⊢}\left({\phi }\wedge {s}\in \left(0,\mathrm{\pi }\right)\right)\to {X}\in ℝ$
418 elioore ${⊢}{s}\in \left(0,\mathrm{\pi }\right)\to {s}\in ℝ$
419 418 adantl ${⊢}\left({\phi }\wedge {s}\in \left(0,\mathrm{\pi }\right)\right)\to {s}\in ℝ$
420 417 419 readdcld ${⊢}\left({\phi }\wedge {s}\in \left(0,\mathrm{\pi }\right)\right)\to {X}+{s}\in ℝ$
421 416 420 ffvelrnd ${⊢}\left({\phi }\wedge {s}\in \left(0,\mathrm{\pi }\right)\right)\to {F}\left({X}+{s}\right)\in ℝ$
422 421 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left(0,\mathrm{\pi }\right)\right)\to {F}\left({X}+{s}\right)\in ℝ$
423 418 371 sylan2 ${⊢}\left({n}\in ℕ\wedge {s}\in \left(0,\mathrm{\pi }\right)\right)\to {D}\left({n}\right)\left({s}\right)\in ℝ$
424 423 adantll ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left(0,\mathrm{\pi }\right)\right)\to {D}\left({n}\right)\left({s}\right)\in ℝ$
425 422 424 remulcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left(0,\mathrm{\pi }\right)\right)\to {F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\in ℝ$
426 ioossicc ${⊢}\left(0,\mathrm{\pi }\right)\subseteq \left[0,\mathrm{\pi }\right]$
427 78 79 76 ltleii ${⊢}-\mathrm{\pi }\le 0$
428 71 leidi ${⊢}\mathrm{\pi }\le \mathrm{\pi }$
429 iccss ${⊢}\left(\left(-\mathrm{\pi }\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\wedge \left(-\mathrm{\pi }\le 0\wedge \mathrm{\pi }\le \mathrm{\pi }\right)\right)\to \left[0,\mathrm{\pi }\right]\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
430 78 71 427 428 429 mp4an ${⊢}\left[0,\mathrm{\pi }\right]\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
431 426 430 sstri ${⊢}\left(0,\mathrm{\pi }\right)\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
432 431 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(0,\mathrm{\pi }\right)\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
433 ioombl ${⊢}\left(0,\mathrm{\pi }\right)\in \mathrm{dom}vol$
434 433 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(0,\mathrm{\pi }\right)\in \mathrm{dom}vol$
435 432 434 396 409 iblss ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({s}\in \left(0,\mathrm{\pi }\right)⟼{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\right)\in {𝐿}^{1}$
436 425 435 itgcl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}\in ℂ$
437 414 415 363 436 fvmptd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({m}\in ℕ⟼{\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}\right)\left({n}\right)={\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}$
438 437 436 eqeltrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({m}\in ℕ⟼{\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}\right)\left({n}\right)\in ℂ$
439 eleq1w ${⊢}{m}={n}\to \left({m}\in ℕ↔{n}\in ℕ\right)$
440 439 anbi2d ${⊢}{m}={n}\to \left(\left({\phi }\wedge {m}\in ℕ\right)↔\left({\phi }\wedge {n}\in ℕ\right)\right)$
441 fveq2 ${⊢}{m}={n}\to {Z}\left({m}\right)={Z}\left({n}\right)$
442 276 340 oveq12d ${⊢}{m}={n}\to {\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}+{\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}={\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}+{\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}$
443 441 442 eqeq12d ${⊢}{m}={n}\to \left({Z}\left({m}\right)={\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}+{\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}↔{Z}\left({n}\right)={\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}+{\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}\right)$
444 440 443 imbi12d ${⊢}{m}={n}\to \left(\left(\left({\phi }\wedge {m}\in ℕ\right)\to {Z}\left({m}\right)={\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}+{\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({m}\right)\left({s}\right)d{s}\right)↔\left(\left({\phi }\wedge {n}\in ℕ\right)\to {Z}\left({n}\right)={\int }_{\left(-\mathrm{\pi },0\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}+{\int }_{\left(0,\mathrm{\pi }\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}\right)\right)$
445 oveq1 ${⊢}{n}={m}\to {n}{x}={m}{x}$
446 445 fveq2d ${⊢}{n}={m}\to \mathrm{cos}{n}{x}=\mathrm{cos}{m}{x}$
447 446 oveq2d ${⊢}{n}={m}\to {F}\left({x}\right)\mathrm{cos}{n}{x}={F}\left({x}\right)\mathrm{cos}{m}{x}$
448 447 adantr ${⊢}\left({n}={m}\wedge {x}\in \left(-\mathrm{\pi },\mathrm{\pi }\right)\right)\to {F}\left({x}\right)\mathrm{cos}{n}{x}={F}\left({x}\right)\mathrm{cos}{m}{x}$
449 448 itgeq2dv ${⊢}{n}={m}\to {\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{n}{x}d{x}={\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{m}{x}d{x}$
450 449 oveq1d ${⊢}{n}={m}\to \frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{n}{x}d{x}}{\mathrm{\pi }}=\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{m}{x}d{x}}{\mathrm{\pi }}$
451 450 cbvmptv ${⊢}\left({n}\in {ℕ}_{0}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{n}{x}d{x}}{\mathrm{\pi }}\right)=\left({m}\in {ℕ}_{0}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{m}{x}d{x}}{\mathrm{\pi }}\right)$
452 20 451 eqtri ${⊢}{A}=\left({m}\in {ℕ}_{0}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{m}{x}d{x}}{\mathrm{\pi }}\right)$
453 445 fveq2d ${⊢}{n}={m}\to \mathrm{sin}{n}{x}=\mathrm{sin}{m}{x}$
454 453 oveq2d ${⊢}{n}={m}\to {F}\left({x}\right)\mathrm{sin}{n}{x}={F}\left({x}\right)\mathrm{sin}{m}{x}$
455 454 adantr ${⊢}\left({n}={m}\wedge {x}\in \left(-\mathrm{\pi },\mathrm{\pi }\right)\right)\to {F}\left({x}\right)\mathrm{sin}{n}{x}={F}\left({x}\right)\mathrm{sin}{m}{x}$
456 455 itgeq2dv ${⊢}{n}={m}\to {\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{n}{x}d{x}={\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{m}{x}d{x}$
457 456 oveq1d ${⊢}{n}={m}\to \frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{n}{x}d{x}}{\mathrm{\pi }}=\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{m}{x}d{x}}{\mathrm{\pi }}$
458 457 cbvmptv ${⊢}\left({n}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{n}{x}d{x}}{\mathrm{\pi }}\right)=\left({m}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{m}{x}d{x}}{\mathrm{\pi }}\right)$
459 21 458 eqtri ${⊢}{B}=\left({m}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{m}{x}d{x}}{\mathrm{\pi }}\right)$
460 fveq2 ${⊢}{n}={k}\to {A}\left({n}\right)={A}\left({k}\right)$
461 oveq1 ${⊢}{n}={k}\to {n}{X}={k}{X}$
462 461 fveq2d ${⊢}{n}={k}\to \mathrm{cos}{n}{X}=\mathrm{cos}{k}{X}$
463 460 462 oveq12d ${⊢}{n}={k}\to {A}\left({n}\right)\mathrm{cos}{n}{X}={A}\left({k}\right)\mathrm{cos}{k}{X}$
464 fveq2 ${⊢}{n}={k}\to {B}\left({n}\right)={B}\left({k}\right)$
465 461 fveq2d ${⊢}{n}={k}\to \mathrm{sin}{n}{X}=\mathrm{sin}{k}{X}$
466 464 465 oveq12d ${⊢}{n}={k}\to {B}\left({n}\right)\mathrm{sin}{n}{X}={B}\left({k}\right)\mathrm{sin}{k}{X}$
467 463 466 oveq12d ${⊢}{n}={k}\to {A}\left({n}\right)\mathrm{cos}{n}{X}+{B}$