# Metamath Proof Explorer

## Theorem fourierdlem88

Description: Given a piecewise continuous function F , a continuous function K and a continuous function S , the function G is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem88.1 ${⊢}{P}=\left({m}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {m}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }+{X}\wedge {p}\left({m}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{m}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}\right)$
fourierdlem88.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
fourierdlem88.x ${⊢}{\phi }\to {X}\in \mathrm{ran}{V}$
fourierdlem88.y ${⊢}{\phi }\to {Y}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
fourierdlem88.w ${⊢}{\phi }\to {W}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
fourierdlem88.h ${⊢}{H}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({s}=0,0,\frac{{F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)}{{s}}\right)\right)$
fourierdlem88.k ${⊢}{K}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({s}=0,1,\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)$
fourierdlem88.u ${⊢}{U}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{H}\left({s}\right){K}\left({s}\right)\right)$
fourierdlem88.n ${⊢}{\phi }\to {N}\in ℝ$
fourierdlem88.s ${⊢}{S}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({N}+\left(\frac{1}{2}\right)\right){s}\right)$
fourierdlem88.g ${⊢}{G}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{U}\left({s}\right){S}\left({s}\right)\right)$
fourierdlem88.m ${⊢}{\phi }\to {M}\in ℕ$
fourierdlem88.v ${⊢}{\phi }\to {V}\in {P}\left({M}\right)$
fourierdlem88.fcn ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
fourierdlem88.r ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {R}\in \left(\left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right){lim}_{ℂ}{V}\left({i}\right)\right)$
fourierdlem88.l ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {L}\in \left(\left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right){lim}_{ℂ}{V}\left({i}+1\right)\right)$
fourierdlem88.q ${⊢}{Q}=\left({i}\in \left(0\dots {M}\right)⟼{V}\left({i}\right)-{X}\right)$
fourierdlem88.o ${⊢}{O}=\left({m}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {m}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }\wedge {p}\left({m}\right)=\mathrm{\pi }\right)\wedge \forall {i}\in \left(0..^{m}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}\right)$
fourierdlem88.i ${⊢}{I}=ℝ\mathrm{D}{F}$
fourierdlem88.ifn ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{I}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)⟶ℝ$
fourierdlem88.c ${⊢}{\phi }\to {C}\in \left(\left({{I}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
fourierdlem88.d ${⊢}{\phi }\to {D}\in \left(\left({{I}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
Assertion fourierdlem88 ${⊢}{\phi }\to {G}\in {𝐿}^{1}$

### Proof

Step Hyp Ref Expression
1 fourierdlem88.1 ${⊢}{P}=\left({m}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {m}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }+{X}\wedge {p}\left({m}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{m}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}\right)$
2 fourierdlem88.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
3 fourierdlem88.x ${⊢}{\phi }\to {X}\in \mathrm{ran}{V}$
4 fourierdlem88.y ${⊢}{\phi }\to {Y}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
5 fourierdlem88.w ${⊢}{\phi }\to {W}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
6 fourierdlem88.h ${⊢}{H}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({s}=0,0,\frac{{F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)}{{s}}\right)\right)$
7 fourierdlem88.k ${⊢}{K}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({s}=0,1,\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)$
8 fourierdlem88.u ${⊢}{U}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{H}\left({s}\right){K}\left({s}\right)\right)$
9 fourierdlem88.n ${⊢}{\phi }\to {N}\in ℝ$
10 fourierdlem88.s ${⊢}{S}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({N}+\left(\frac{1}{2}\right)\right){s}\right)$
11 fourierdlem88.g ${⊢}{G}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{U}\left({s}\right){S}\left({s}\right)\right)$
12 fourierdlem88.m ${⊢}{\phi }\to {M}\in ℕ$
13 fourierdlem88.v ${⊢}{\phi }\to {V}\in {P}\left({M}\right)$
14 fourierdlem88.fcn ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
15 fourierdlem88.r ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {R}\in \left(\left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right){lim}_{ℂ}{V}\left({i}\right)\right)$
16 fourierdlem88.l ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {L}\in \left(\left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right){lim}_{ℂ}{V}\left({i}+1\right)\right)$
17 fourierdlem88.q ${⊢}{Q}=\left({i}\in \left(0\dots {M}\right)⟼{V}\left({i}\right)-{X}\right)$
18 fourierdlem88.o ${⊢}{O}=\left({m}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {m}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }\wedge {p}\left({m}\right)=\mathrm{\pi }\right)\wedge \forall {i}\in \left(0..^{m}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}\right)$
19 fourierdlem88.i ${⊢}{I}=ℝ\mathrm{D}{F}$
20 fourierdlem88.ifn ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{I}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)⟶ℝ$
21 fourierdlem88.c ${⊢}{\phi }\to {C}\in \left(\left({{I}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
22 fourierdlem88.d ${⊢}{\phi }\to {D}\in \left(\left({{I}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
23 pire ${⊢}\mathrm{\pi }\in ℝ$
24 23 a1i ${⊢}{\phi }\to \mathrm{\pi }\in ℝ$
25 24 renegcld ${⊢}{\phi }\to -\mathrm{\pi }\in ℝ$
26 1 fourierdlem2 ${⊢}{M}\in ℕ\to \left({V}\in {P}\left({M}\right)↔\left({V}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)\wedge \left(\left({V}\left(0\right)=-\mathrm{\pi }+{X}\wedge {V}\left({M}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{V}\left({i}\right)<{V}\left({i}+1\right)\right)\right)\right)$
27 12 26 syl ${⊢}{\phi }\to \left({V}\in {P}\left({M}\right)↔\left({V}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)\wedge \left(\left({V}\left(0\right)=-\mathrm{\pi }+{X}\wedge {V}\left({M}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{V}\left({i}\right)<{V}\left({i}+1\right)\right)\right)\right)$
28 13 27 mpbid ${⊢}{\phi }\to \left({V}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)\wedge \left(\left({V}\left(0\right)=-\mathrm{\pi }+{X}\wedge {V}\left({M}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{V}\left({i}\right)<{V}\left({i}+1\right)\right)\right)$
29 28 simpld ${⊢}{\phi }\to {V}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)$
30 elmapi ${⊢}{V}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)\to {V}:\left(0\dots {M}\right)⟶ℝ$
31 frn ${⊢}{V}:\left(0\dots {M}\right)⟶ℝ\to \mathrm{ran}{V}\subseteq ℝ$
32 29 30 31 3syl ${⊢}{\phi }\to \mathrm{ran}{V}\subseteq ℝ$
33 32 3 sseldd ${⊢}{\phi }\to {X}\in ℝ$
34 25 24 33 1 18 12 13 17 fourierdlem14 ${⊢}{\phi }\to {Q}\in {O}\left({M}\right)$
35 ioossre ${⊢}\left({X},\mathrm{+\infty }\right)\subseteq ℝ$
36 35 a1i ${⊢}{\phi }\to \left({X},\mathrm{+\infty }\right)\subseteq ℝ$
37 2 36 fssresd ${⊢}{\phi }\to \left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right):\left({X},\mathrm{+\infty }\right)⟶ℝ$
38 ax-resscn ${⊢}ℝ\subseteq ℂ$
39 36 38 sstrdi ${⊢}{\phi }\to \left({X},\mathrm{+\infty }\right)\subseteq ℂ$
40 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
41 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
42 41 a1i ${⊢}{\phi }\to \mathrm{+\infty }\in {ℝ}^{*}$
43 33 ltpnfd ${⊢}{\phi }\to {X}<\mathrm{+\infty }$
44 40 42 33 43 lptioo1cn ${⊢}{\phi }\to {X}\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(\left({X},\mathrm{+\infty }\right)\right)$
45 37 39 44 4 limcrecl ${⊢}{\phi }\to {Y}\in ℝ$
46 ioossre ${⊢}\left(\mathrm{-\infty },{X}\right)\subseteq ℝ$
47 46 a1i ${⊢}{\phi }\to \left(\mathrm{-\infty },{X}\right)\subseteq ℝ$
48 2 47 fssresd ${⊢}{\phi }\to \left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right):\left(\mathrm{-\infty },{X}\right)⟶ℝ$
49 47 38 sstrdi ${⊢}{\phi }\to \left(\mathrm{-\infty },{X}\right)\subseteq ℂ$
50 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
51 50 a1i ${⊢}{\phi }\to \mathrm{-\infty }\in {ℝ}^{*}$
52 33 mnfltd ${⊢}{\phi }\to \mathrm{-\infty }<{X}$
53 40 51 33 52 lptioo2cn ${⊢}{\phi }\to {X}\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(\left(\mathrm{-\infty },{X}\right)\right)$
54 48 49 53 5 limcrecl ${⊢}{\phi }\to {W}\in ℝ$
55 2 33 45 54 6 7 8 fourierdlem55 ${⊢}{\phi }\to {U}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
56 55 ffvelrnda ${⊢}\left({\phi }\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {U}\left({s}\right)\in ℝ$
57 10 fourierdlem5 ${⊢}{N}\in ℝ\to {S}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
58 9 57 syl ${⊢}{\phi }\to {S}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
59 58 ffvelrnda ${⊢}\left({\phi }\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {S}\left({s}\right)\in ℝ$
60 56 59 remulcld ${⊢}\left({\phi }\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {U}\left({s}\right){S}\left({s}\right)\in ℝ$
61 60 recnd ${⊢}\left({\phi }\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {U}\left({s}\right){S}\left({s}\right)\in ℂ$
62 61 11 fmptd ${⊢}{\phi }\to {G}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℂ$
63 ssid ${⊢}ℂ\subseteq ℂ$
64 cncfss
65 38 63 64 mp2an
66 2 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {F}:ℝ⟶ℝ$
67 18 12 34 fourierdlem15 ${⊢}{\phi }\to {Q}:\left(0\dots {M}\right)⟶\left[-\mathrm{\pi },\mathrm{\pi }\right]$
68 67 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}:\left(0\dots {M}\right)⟶\left[-\mathrm{\pi },\mathrm{\pi }\right]$
69 elfzofz ${⊢}{i}\in \left(0..^{M}\right)\to {i}\in \left(0\dots {M}\right)$
70 69 adantl ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {i}\in \left(0\dots {M}\right)$
71 68 70 ffvelrnd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}\right)\in \left[-\mathrm{\pi },\mathrm{\pi }\right]$
72 fzofzp1 ${⊢}{i}\in \left(0..^{M}\right)\to {i}+1\in \left(0\dots {M}\right)$
73 72 adantl ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {i}+1\in \left(0\dots {M}\right)$
74 68 73 ffvelrnd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}+1\right)\in \left[-\mathrm{\pi },\mathrm{\pi }\right]$
75 33 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {X}\in ℝ$
76 1 12 13 3 fourierdlem12 ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to ¬{X}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)$
77 75 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {X}\in ℂ$
78 77 addid2d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to 0+{X}={X}$
79 23 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \mathrm{\pi }\in ℝ$
80 79 renegcld ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to -\mathrm{\pi }\in ℝ$
81 80 75 readdcld ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to -\mathrm{\pi }+{X}\in ℝ$
82 79 75 readdcld ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \mathrm{\pi }+{X}\in ℝ$
83 81 82 iccssred ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]\subseteq ℝ$
84 1 12 13 fourierdlem15 ${⊢}{\phi }\to {V}:\left(0\dots {M}\right)⟶\left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]$
85 84 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {V}:\left(0\dots {M}\right)⟶\left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]$
86 85 70 ffvelrnd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {V}\left({i}\right)\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]$
87 83 86 sseldd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {V}\left({i}\right)\in ℝ$
88 87 75 resubcld ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {V}\left({i}\right)-{X}\in ℝ$
89 17 fvmpt2 ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {V}\left({i}\right)-{X}\in ℝ\right)\to {Q}\left({i}\right)={V}\left({i}\right)-{X}$
90 70 88 89 syl2anc ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}\right)={V}\left({i}\right)-{X}$
91 90 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}\right)+{X}={V}\left({i}\right)-{X}+{X}$
92 87 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {V}\left({i}\right)\in ℂ$
93 92 77 npcand ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {V}\left({i}\right)-{X}+{X}={V}\left({i}\right)$
94 91 93 eqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}\right)+{X}={V}\left({i}\right)$
95 fveq2 ${⊢}{i}={j}\to {V}\left({i}\right)={V}\left({j}\right)$
96 95 oveq1d ${⊢}{i}={j}\to {V}\left({i}\right)-{X}={V}\left({j}\right)-{X}$
97 96 cbvmptv ${⊢}\left({i}\in \left(0\dots {M}\right)⟼{V}\left({i}\right)-{X}\right)=\left({j}\in \left(0\dots {M}\right)⟼{V}\left({j}\right)-{X}\right)$
98 17 97 eqtri ${⊢}{Q}=\left({j}\in \left(0\dots {M}\right)⟼{V}\left({j}\right)-{X}\right)$
99 98 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}=\left({j}\in \left(0\dots {M}\right)⟼{V}\left({j}\right)-{X}\right)$
100 simpr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {j}={i}+1\right)\to {j}={i}+1$
101 100 fveq2d ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {j}={i}+1\right)\to {V}\left({j}\right)={V}\left({i}+1\right)$
102 101 oveq1d ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {j}={i}+1\right)\to {V}\left({j}\right)-{X}={V}\left({i}+1\right)-{X}$
103 85 73 ffvelrnd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {V}\left({i}+1\right)\in \left[-\mathrm{\pi }+{X},\mathrm{\pi }+{X}\right]$
104 83 103 sseldd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {V}\left({i}+1\right)\in ℝ$
105 104 75 resubcld ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {V}\left({i}+1\right)-{X}\in ℝ$
106 99 102 73 105 fvmptd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}+1\right)={V}\left({i}+1\right)-{X}$
107 106 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}+1\right)+{X}={V}\left({i}+1\right)-{X}+{X}$
108 104 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {V}\left({i}+1\right)\in ℂ$
109 108 77 npcand ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {V}\left({i}+1\right)-{X}+{X}={V}\left({i}+1\right)$
110 107 109 eqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}+1\right)+{X}={V}\left({i}+1\right)$
111 94 110 oveq12d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({Q}\left({i}\right)+{X},{Q}\left({i}+1\right)+{X}\right)=\left({V}\left({i}\right),{V}\left({i}+1\right)\right)$
112 78 111 eleq12d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left(0+{X}\in \left({Q}\left({i}\right)+{X},{Q}\left({i}+1\right)+{X}\right)↔{X}\in \left({V}\left({i}\right),{V}\left({i}+1\right)\right)\right)$
113 76 112 mtbird ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to ¬0+{X}\in \left({Q}\left({i}\right)+{X},{Q}\left({i}+1\right)+{X}\right)$
114 0red ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to 0\in ℝ$
115 90 88 eqeltrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}\right)\in ℝ$
116 106 105 eqeltrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}+1\right)\in ℝ$
117 114 115 116 75 eliooshift ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left(0\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)↔0+{X}\in \left({Q}\left({i}\right)+{X},{Q}\left({i}+1\right)+{X}\right)\right)$
118 113 117 mtbird ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to ¬0\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)$
119 111 reseq2d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {{F}↾}_{\left({Q}\left({i}\right)+{X},{Q}\left({i}+1\right)+{X}\right)}={{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}$
120 111 oveq1d
121 14 119 120 3eltr4d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{F}↾}_{\left({Q}\left({i}\right)+{X},{Q}\left({i}+1\right)+{X}\right)}\right):\left({Q}\left({i}\right)+{X},{Q}\left({i}+1\right)+{X}\right)\underset{cn}{⟶}ℂ$
122 45 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Y}\in ℝ$
123 54 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\in ℝ$
124 9 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {N}\in ℝ$
125 66 71 74 75 118 121 122 123 6 7 8 124 10 11 fourierdlem78 ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{G}↾}_{\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}{⟶}ℝ$
126 65 125 sseldi ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{G}↾}_{\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}{⟶}ℂ$
127 eqid ${⊢}\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{U}\left({s}\right)\right)=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{U}\left({s}\right)\right)$
128 eqid ${⊢}\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{S}\left({s}\right)\right)=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{S}\left({s}\right)\right)$
129 eqid ${⊢}\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{U}\left({s}\right){S}\left({s}\right)\right)=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{U}\left({s}\right){S}\left({s}\right)\right)$
130 23 renegcli ${⊢}-\mathrm{\pi }\in ℝ$
131 130 rexri ${⊢}-\mathrm{\pi }\in {ℝ}^{*}$
132 131 a1i ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to -\mathrm{\pi }\in {ℝ}^{*}$
133 23 rexri ${⊢}\mathrm{\pi }\in {ℝ}^{*}$
134 133 a1i ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to \mathrm{\pi }\in {ℝ}^{*}$
135 68 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {Q}:\left(0\dots {M}\right)⟶\left[-\mathrm{\pi },\mathrm{\pi }\right]$
136 simplr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {i}\in \left(0..^{M}\right)$
137 132 134 135 136 fourierdlem8 ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to \left[{Q}\left({i}\right),{Q}\left({i}+1\right)\right]\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
138 ioossicc ${⊢}\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\subseteq \left[{Q}\left({i}\right),{Q}\left({i}+1\right)\right]$
139 138 sseli ${⊢}{s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\to {s}\in \left[{Q}\left({i}\right),{Q}\left({i}+1\right)\right]$
140 139 adantl ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {s}\in \left[{Q}\left({i}\right),{Q}\left({i}+1\right)\right]$
141 137 140 sseldd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]$
142 2 33 45 54 6 fourierdlem9 ${⊢}{\phi }\to {H}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
143 142 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {H}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
144 143 141 ffvelrnd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {H}\left({s}\right)\in ℝ$
145 7 fourierdlem43 ${⊢}{K}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
146 145 a1i ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {K}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
147 146 141 ffvelrnd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {K}\left({s}\right)\in ℝ$
148 144 147 remulcld ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {H}\left({s}\right){K}\left({s}\right)\in ℝ$
149 8 fvmpt2 ${⊢}\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge {H}\left({s}\right){K}\left({s}\right)\in ℝ\right)\to {U}\left({s}\right)={H}\left({s}\right){K}\left({s}\right)$
150 141 148 149 syl2anc ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {U}\left({s}\right)={H}\left({s}\right){K}\left({s}\right)$
151 150 148 eqeltrd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {U}\left({s}\right)\in ℝ$
152 151 recnd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {U}\left({s}\right)\in ℂ$
153 9 10 fourierdlem18 ${⊢}{\phi }\to {S}:\left[-\mathrm{\pi },\mathrm{\pi }\right]\underset{cn}{⟶}ℝ$
154 cncff ${⊢}{S}:\left[-\mathrm{\pi },\mathrm{\pi }\right]\underset{cn}{⟶}ℝ\to {S}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
155 153 154 syl ${⊢}{\phi }\to {S}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
156 155 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {S}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
157 156 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {S}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
158 157 141 ffvelrnd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {S}\left({s}\right)\in ℝ$
159 158 recnd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {S}\left({s}\right)\in ℂ$
160 eqid ${⊢}\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{H}\left({s}\right)\right)=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{H}\left({s}\right)\right)$
161 eqid ${⊢}\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{K}\left({s}\right)\right)=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{K}\left({s}\right)\right)$
162 eqid ${⊢}\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{H}\left({s}\right){K}\left({s}\right)\right)=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{H}\left({s}\right){K}\left({s}\right)\right)$
163 144 recnd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {H}\left({s}\right)\in ℂ$
164 147 recnd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {K}\left({s}\right)\in ℂ$
165 38 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to ℝ\subseteq ℂ$
166 20 165 fssd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{I}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)⟶ℂ$
167 eqid ${⊢}if\left({V}\left({i}\right)={X},{D},\frac{{R}-if\left({V}\left({i}\right)<{X},{W},{Y}\right)}{{Q}\left({i}\right)}\right)=if\left({V}\left({i}\right)={X},{D},\frac{{R}-if\left({V}\left({i}\right)<{X},{W},{Y}\right)}{{Q}\left({i}\right)}\right)$
168 33 1 2 3 4 54 6 12 13 15 17 18 19 166 22 167 fourierdlem75 ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to if\left({V}\left({i}\right)={X},{D},\frac{{R}-if\left({V}\left({i}\right)<{X},{W},{Y}\right)}{{Q}\left({i}\right)}\right)\in \left(\left({{H}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)\right)$
169 142 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {H}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
170 131 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to -\mathrm{\pi }\in {ℝ}^{*}$
171 133 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \mathrm{\pi }\in {ℝ}^{*}$
172 simpr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {i}\in \left(0..^{M}\right)$
173 170 171 68 172 fourierdlem8 ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left[{Q}\left({i}\right),{Q}\left({i}+1\right)\right]\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
174 138 173 sstrid ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
175 169 174 feqresmpt ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {{H}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{H}\left({s}\right)\right)$
176 175 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{H}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{H}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}\right)$
177 168 176 eleqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to if\left({V}\left({i}\right)={X},{D},\frac{{R}-if\left({V}\left({i}\right)<{X},{W},{Y}\right)}{{Q}\left({i}\right)}\right)\in \left(\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{H}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}\right)\right)$
178 limcresi ${⊢}{K}{lim}_{ℂ}{Q}\left({i}\right)\subseteq \left({{K}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)$
179 7 fourierdlem62 ${⊢}{K}:\left[-\mathrm{\pi },\mathrm{\pi }\right]\underset{cn}{⟶}ℝ$
180 179 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {K}:\left[-\mathrm{\pi },\mathrm{\pi }\right]\underset{cn}{⟶}ℝ$
181 180 71 cnlimci ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {K}\left({Q}\left({i}\right)\right)\in \left({K}{lim}_{ℂ}{Q}\left({i}\right)\right)$
182 178 181 sseldi ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {K}\left({Q}\left({i}\right)\right)\in \left(\left({{K}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)\right)$
183 145 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {K}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
184 183 174 feqresmpt ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {{K}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{K}\left({s}\right)\right)$
185 184 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{K}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{K}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}\right)$
186 182 185 eleqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {K}\left({Q}\left({i}\right)\right)\in \left(\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{K}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}\right)\right)$
187 160 161 162 163 164 177 186 mullimc ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to if\left({V}\left({i}\right)={X},{D},\frac{{R}-if\left({V}\left({i}\right)<{X},{W},{Y}\right)}{{Q}\left({i}\right)}\right){K}\left({Q}\left({i}\right)\right)\in \left(\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{H}\left({s}\right){K}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}\right)\right)$
188 150 eqcomd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {H}\left({s}\right){K}\left({s}\right)={U}\left({s}\right)$
189 188 mpteq2dva ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{H}\left({s}\right){K}\left({s}\right)\right)=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{U}\left({s}\right)\right)$
190 189 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{H}\left({s}\right){K}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}\right)=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{U}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}\right)$
191 187 190 eleqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to if\left({V}\left({i}\right)={X},{D},\frac{{R}-if\left({V}\left({i}\right)<{X},{W},{Y}\right)}{{Q}\left({i}\right)}\right){K}\left({Q}\left({i}\right)\right)\in \left(\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{U}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}\right)\right)$
192 limcresi ${⊢}{S}{lim}_{ℂ}{Q}\left({i}\right)\subseteq \left({{S}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)$
193 153 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {S}:\left[-\mathrm{\pi },\mathrm{\pi }\right]\underset{cn}{⟶}ℝ$
194 193 71 cnlimci ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {S}\left({Q}\left({i}\right)\right)\in \left({S}{lim}_{ℂ}{Q}\left({i}\right)\right)$
195 192 194 sseldi ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {S}\left({Q}\left({i}\right)\right)\in \left(\left({{S}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)\right)$
196 156 174 feqresmpt ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {{S}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{S}\left({s}\right)\right)$
197 196 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{S}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{S}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}\right)$
198 195 197 eleqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {S}\left({Q}\left({i}\right)\right)\in \left(\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{S}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}\right)\right)$
199 127 128 129 152 159 191 198 mullimc ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to if\left({V}\left({i}\right)={X},{D},\frac{{R}-if\left({V}\left({i}\right)<{X},{W},{Y}\right)}{{Q}\left({i}\right)}\right){K}\left({Q}\left({i}\right)\right){S}\left({Q}\left({i}\right)\right)\in \left(\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{U}\left({s}\right){S}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}\right)\right)$
200 60 11 fmptd ${⊢}{\phi }\to {G}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
201 200 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {G}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
202 201 174 feqresmpt ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {{G}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{G}\left({s}\right)\right)$
203 151 158 remulcld ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {U}\left({s}\right){S}\left({s}\right)\in ℝ$
204 11 fvmpt2 ${⊢}\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\wedge {U}\left({s}\right){S}\left({s}\right)\in ℝ\right)\to {G}\left({s}\right)={U}\left({s}\right){S}\left({s}\right)$
205 141 203 204 syl2anc ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to {G}\left({s}\right)={U}\left({s}\right){S}\left({s}\right)$
206 205 mpteq2dva ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{G}\left({s}\right)\right)=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{U}\left({s}\right){S}\left({s}\right)\right)$
207 202 206 eqtr2d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{U}\left({s}\right){S}\left({s}\right)\right)={{G}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}$
208 207 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{U}\left({s}\right){S}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}\right)=\left({{G}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)$
209 199 208 eleqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to if\left({V}\left({i}\right)={X},{D},\frac{{R}-if\left({V}\left({i}\right)<{X},{W},{Y}\right)}{{Q}\left({i}\right)}\right){K}\left({Q}\left({i}\right)\right){S}\left({Q}\left({i}\right)\right)\in \left(\left({{G}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)\right)$
210 eqid ${⊢}if\left({V}\left({i}+1\right)={X},{C},\frac{{L}-if\left({V}\left({i}+1\right)<{X},{W},{Y}\right)}{{Q}\left({i}+1\right)}\right)=if\left({V}\left({i}+1\right)={X},{C},\frac{{L}-if\left({V}\left({i}+1\right)<{X},{W},{Y}\right)}{{Q}\left({i}+1\right)}\right)$
211 33 1 2 3 45 5 6 12 13 16 17 18 19 20 21 210 fourierdlem74 ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to if\left({V}\left({i}+1\right)={X},{C},\frac{{L}-if\left({V}\left({i}+1\right)<{X},{W},{Y}\right)}{{Q}\left({i}+1\right)}\right)\in \left(\left({{H}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)\right)$
212 175 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{H}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{H}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}+1\right)$
213 211 212 eleqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to if\left({V}\left({i}+1\right)={X},{C},\frac{{L}-if\left({V}\left({i}+1\right)<{X},{W},{Y}\right)}{{Q}\left({i}+1\right)}\right)\in \left(\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{H}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}+1\right)\right)$
214 limcresi ${⊢}{K}{lim}_{ℂ}{Q}\left({i}+1\right)\subseteq \left({{K}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)$
215 180 74 cnlimci ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {K}\left({Q}\left({i}+1\right)\right)\in \left({K}{lim}_{ℂ}{Q}\left({i}+1\right)\right)$
216 214 215 sseldi ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {K}\left({Q}\left({i}+1\right)\right)\in \left(\left({{K}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)\right)$
217 184 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{K}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{K}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}+1\right)$
218 216 217 eleqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {K}\left({Q}\left({i}+1\right)\right)\in \left(\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{K}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}+1\right)\right)$
219 160 161 162 163 164 213 218 mullimc ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to if\left({V}\left({i}+1\right)={X},{C},\frac{{L}-if\left({V}\left({i}+1\right)<{X},{W},{Y}\right)}{{Q}\left({i}+1\right)}\right){K}\left({Q}\left({i}+1\right)\right)\in \left(\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{H}\left({s}\right){K}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}+1\right)\right)$
220 189 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{H}\left({s}\right){K}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}+1\right)=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{U}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}+1\right)$
221 219 220 eleqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to if\left({V}\left({i}+1\right)={X},{C},\frac{{L}-if\left({V}\left({i}+1\right)<{X},{W},{Y}\right)}{{Q}\left({i}+1\right)}\right){K}\left({Q}\left({i}+1\right)\right)\in \left(\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{U}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}+1\right)\right)$
222 limcresi ${⊢}{S}{lim}_{ℂ}{Q}\left({i}+1\right)\subseteq \left({{S}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)$
223 193 74 cnlimci ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {S}\left({Q}\left({i}+1\right)\right)\in \left({S}{lim}_{ℂ}{Q}\left({i}+1\right)\right)$
224 222 223 sseldi ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {S}\left({Q}\left({i}+1\right)\right)\in \left(\left({{S}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)\right)$
225 196 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{S}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)=\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{S}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}+1\right)$
226 224 225 eleqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {S}\left({Q}\left({i}+1\right)\right)\in \left(\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{S}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}+1\right)\right)$
227 127 128 129 152 159 221 226 mullimc ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to if\left({V}\left({i}+1\right)={X},{C},\frac{{L}-if\left({V}\left({i}+1\right)<{X},{W},{Y}\right)}{{Q}\left({i}+1\right)}\right){K}\left({Q}\left({i}+1\right)\right){S}\left({Q}\left({i}+1\right)\right)\in \left(\left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{U}\left({s}\right){S}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}+1\right)\right)$
228 207 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{U}\left({s}\right){S}\left({s}\right)\right){lim}_{ℂ}{Q}\left({i}+1\right)=\left({{G}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)$
229 227 228 eleqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to if\left({V}\left({i}+1\right)={X},{C},\frac{{L}-if\left({V}\left({i}+1\right)<{X},{W},{Y}\right)}{{Q}\left({i}+1\right)}\right){K}\left({Q}\left({i}+1\right)\right){S}\left({Q}\left({i}+1\right)\right)\in \left(\left({{G}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)\right)$
230 18 12 34 62 126 209 229 fourierdlem69 ${⊢}{\phi }\to {G}\in {𝐿}^{1}$