# Metamath Proof Explorer

## Theorem fourierdlem111

Description: The fourier partial sum for F is the sum of two integrals, with the same integrand involving F and the Dirichlet Kernel D , but on two opposite intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem111.a ${⊢}{A}=\left({n}\in {ℕ}_{0}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({t}\right)\mathrm{cos}{n}{t}d{t}}{\mathrm{\pi }}\right)$
fourierdlem111.b ${⊢}{B}=\left({n}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({t}\right)\mathrm{sin}{n}{t}d{t}}{\mathrm{\pi }}\right)$
fourierdlem111.s ${⊢}{S}=\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)$
fourierdlem111.d ${⊢}{D}=\left({n}\in ℕ⟼\left({y}\in ℝ⟼if\left({y}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{n}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){y}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{y}}{2}\right)}\right)\right)\right)$
fourierdlem111.p ${⊢}{P}=\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)$
fourierdlem111.m ${⊢}{\phi }\to {M}\in ℕ$
fourierdlem111.q ${⊢}{\phi }\to {Q}\in {P}\left({M}\right)$
fourierdlem111.x ${⊢}{\phi }\to {X}\in ℝ$
fourierdlem111.6 ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
fourierdlem111.fper ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)$
fourierdlem111.g ${⊢}{G}=\left({x}\in ℝ⟼{F}\left({X}+{x}\right){D}\left({n}\right)\left({x}\right)\right)$
fourierdlem111.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}{⟶}ℂ$
fourierdlem111.r ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {R}\in \left(\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)\right)$
fourierdlem111.l ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {L}\in \left(\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)\right)$
fourierdlem111.t ${⊢}{T}=2\mathrm{\pi }$
fourierdlem111.o ${⊢}{O}=\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)$
fourierdlem111.14 ${⊢}{W}=\left({i}\in \left(0\dots {M}\right)⟼{Q}\left({i}\right)-{X}\right)$
Assertion fourierdlem111 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {S}\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}$

### Proof

Step Hyp Ref Expression
1 fourierdlem111.a ${⊢}{A}=\left({n}\in {ℕ}_{0}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({t}\right)\mathrm{cos}{n}{t}d{t}}{\mathrm{\pi }}\right)$
2 fourierdlem111.b ${⊢}{B}=\left({n}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({t}\right)\mathrm{sin}{n}{t}d{t}}{\mathrm{\pi }}\right)$
3 fourierdlem111.s ${⊢}{S}=\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)$
4 fourierdlem111.d ${⊢}{D}=\left({n}\in ℕ⟼\left({y}\in ℝ⟼if\left({y}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{n}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){y}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{y}}{2}\right)}\right)\right)\right)$
5 fourierdlem111.p ${⊢}{P}=\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)$
6 fourierdlem111.m ${⊢}{\phi }\to {M}\in ℕ$
7 fourierdlem111.q ${⊢}{\phi }\to {Q}\in {P}\left({M}\right)$
8 fourierdlem111.x ${⊢}{\phi }\to {X}\in ℝ$
9 fourierdlem111.6 ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
10 fourierdlem111.fper ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)$
11 fourierdlem111.g ${⊢}{G}=\left({x}\in ℝ⟼{F}\left({X}+{x}\right){D}\left({n}\right)\left({x}\right)\right)$
12 fourierdlem111.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 fourierdlem111.r ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {R}\in \left(\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)\right)$
14 fourierdlem111.l ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {L}\in \left(\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)\right)$
15 fourierdlem111.t ${⊢}{T}=2\mathrm{\pi }$
16 fourierdlem111.o ${⊢}{O}=\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)$
17 fourierdlem111.14 ${⊢}{W}=\left({i}\in \left(0\dots {M}\right)⟼{Q}\left({i}\right)-{X}\right)$
18 eleq1 ${⊢}{k}={n}\to \left({k}\in ℕ↔{n}\in ℕ\right)$
19 18 anbi2d ${⊢}{k}={n}\to \left(\left({\phi }\wedge {k}\in ℕ\right)↔\left({\phi }\wedge {n}\in ℕ\right)\right)$
20 fveq2 ${⊢}{k}={n}\to {S}\left({k}\right)={S}\left({n}\right)$
21 fveq2 ${⊢}{k}={n}\to {D}\left({k}\right)={D}\left({n}\right)$
22 21 fveq1d ${⊢}{k}={n}\to {D}\left({k}\right)\left({t}-{X}\right)={D}\left({n}\right)\left({t}-{X}\right)$
23 22 oveq2d ${⊢}{k}={n}\to {F}\left({t}\right){D}\left({k}\right)\left({t}-{X}\right)={F}\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)$
24 23 adantr ${⊢}\left({k}={n}\wedge {t}\in \left(-\mathrm{\pi },\mathrm{\pi }\right)\right)\to {F}\left({t}\right){D}\left({k}\right)\left({t}-{X}\right)={F}\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)$
25 24 itgeq2dv ${⊢}{k}={n}\to {\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({t}\right){D}\left({k}\right)\left({t}-{X}\right)d{t}={\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)d{t}$
26 20 25 eqeq12d ${⊢}{k}={n}\to \left({S}\left({k}\right)={\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({t}\right){D}\left({k}\right)\left({t}-{X}\right)d{t}↔{S}\left({n}\right)={\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)d{t}\right)$
27 19 26 imbi12d ${⊢}{k}={n}\to \left(\left(\left({\phi }\wedge {k}\in ℕ\right)\to {S}\left({k}\right)={\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({t}\right){D}\left({k}\right)\left({t}-{X}\right)d{t}\right)↔\left(\left({\phi }\wedge {n}\in ℕ\right)\to {S}\left({n}\right)={\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)d{t}\right)\right)$
28 9 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}:ℝ⟶ℝ$
29 eqid ${⊢}\left(-\mathrm{\pi },\mathrm{\pi }\right)=\left(-\mathrm{\pi },\mathrm{\pi }\right)$
30 ioossre ${⊢}\left(-\mathrm{\pi },\mathrm{\pi }\right)\subseteq ℝ$
31 30 a1i ${⊢}{\phi }\to \left(-\mathrm{\pi },\mathrm{\pi }\right)\subseteq ℝ$
32 9 31 feqresmpt ${⊢}{\phi }\to {{F}↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}=\left({x}\in \left(-\mathrm{\pi },\mathrm{\pi }\right)⟼{F}\left({x}\right)\right)$
33 ioossicc ${⊢}\left(-\mathrm{\pi },\mathrm{\pi }\right)\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
34 33 a1i ${⊢}{\phi }\to \left(-\mathrm{\pi },\mathrm{\pi }\right)\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
35 ioombl ${⊢}\left(-\mathrm{\pi },\mathrm{\pi }\right)\in \mathrm{dom}vol$
36 35 a1i ${⊢}{\phi }\to \left(-\mathrm{\pi },\mathrm{\pi }\right)\in \mathrm{dom}vol$
37 9 adantr ${⊢}\left({\phi }\wedge {x}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {F}:ℝ⟶ℝ$
38 pire ${⊢}\mathrm{\pi }\in ℝ$
39 38 renegcli ${⊢}-\mathrm{\pi }\in ℝ$
40 39 38 elicc2i ${⊢}{t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]↔\left({t}\in ℝ\wedge -\mathrm{\pi }\le {t}\wedge {t}\le \mathrm{\pi }\right)$
41 40 simp1bi ${⊢}{t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\to {t}\in ℝ$
42 41 ssriv ${⊢}\left[-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℝ$
43 42 a1i ${⊢}{\phi }\to \left[-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℝ$
44 43 sselda ${⊢}\left({\phi }\wedge {x}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {x}\in ℝ$
45 37 44 ffvelrnd ${⊢}\left({\phi }\wedge {x}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {F}\left({x}\right)\in ℝ$
46 9 43 feqresmpt ${⊢}{\phi }\to {{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}=\left({x}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{F}\left({x}\right)\right)$
47 ax-resscn ${⊢}ℝ\subseteq ℂ$
48 47 a1i ${⊢}{\phi }\to ℝ\subseteq ℂ$
49 9 48 fssd ${⊢}{\phi }\to {F}:ℝ⟶ℂ$
50 49 43 fssresd ${⊢}{\phi }\to \left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right):\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℂ$
51 ioossicc ${⊢}\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\subseteq \left[{Q}\left({i}\right),{Q}\left({i}+1\right)\right]$
52 39 rexri ${⊢}-\mathrm{\pi }\in {ℝ}^{*}$
53 52 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to -\mathrm{\pi }\in {ℝ}^{*}$
54 38 rexri ${⊢}\mathrm{\pi }\in {ℝ}^{*}$
55 54 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \mathrm{\pi }\in {ℝ}^{*}$
56 5 6 7 fourierdlem15 ${⊢}{\phi }\to {Q}:\left(0\dots {M}\right)⟶\left[-\mathrm{\pi },\mathrm{\pi }\right]$
57 56 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}:\left(0\dots {M}\right)⟶\left[-\mathrm{\pi },\mathrm{\pi }\right]$
58 simpr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {i}\in \left(0..^{M}\right)$
59 53 55 57 58 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]$
60 51 59 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]$
61 60 resabs1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}={{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}$
62 61 12 eqeltrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)↾}_{\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}{⟶}ℂ$
63 61 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)=\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)$
64 13 63 eleqtrrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {R}\in \left(\left({\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)\right)$
65 61 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)=\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)$
66 14 65 eleqtrrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {L}\in \left(\left({\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)\right)$
67 5 6 7 50 62 64 66 fourierdlem69 ${⊢}{\phi }\to {{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\in {𝐿}^{1}$
68 46 67 eqeltrrd ${⊢}{\phi }\to \left({x}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{F}\left({x}\right)\right)\in {𝐿}^{1}$
69 34 36 45 68 iblss ${⊢}{\phi }\to \left({x}\in \left(-\mathrm{\pi },\mathrm{\pi }\right)⟼{F}\left({x}\right)\right)\in {𝐿}^{1}$
70 32 69 eqeltrd ${⊢}{\phi }\to {{F}↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}\in {𝐿}^{1}$
71 70 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {{F}↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}\in {𝐿}^{1}$
72 8 adantr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {X}\in ℝ$
73 simpr ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {k}\in ℕ$
74 28 29 71 1 2 72 3 4 73 fourierdlem83 ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {S}\left({k}\right)={\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({t}\right){D}\left({k}\right)\left({t}-{X}\right)d{t}$
75 27 74 chvarvv ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {S}\left({n}\right)={\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)d{t}$
76 39 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to -\mathrm{\pi }\in ℝ$
77 38 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \mathrm{\pi }\in ℝ$
78 49 adantr ${⊢}\left({\phi }\wedge {t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {F}:ℝ⟶ℂ$
79 41 adantl ${⊢}\left({\phi }\wedge {t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {t}\in ℝ$
80 78 79 ffvelrnd ${⊢}\left({\phi }\wedge {t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {F}\left({t}\right)\in ℂ$
81 80 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {F}\left({t}\right)\in ℂ$
82 4 dirkerf ${⊢}{n}\in ℕ\to {D}\left({n}\right):ℝ⟶ℝ$
83 82 ad2antlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {D}\left({n}\right):ℝ⟶ℝ$
84 8 adantr ${⊢}\left({\phi }\wedge {t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {X}\in ℝ$
85 79 84 resubcld ${⊢}\left({\phi }\wedge {t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {t}-{X}\in ℝ$
86 85 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {t}-{X}\in ℝ$
87 83 86 ffvelrnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {D}\left({n}\right)\left({t}-{X}\right)\in ℝ$
88 87 recnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {D}\left({n}\right)\left({t}-{X}\right)\in ℂ$
89 81 88 mulcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {F}\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)\in ℂ$
90 76 77 89 itgioo ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)d{t}={\int }_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}{F}\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)d{t}$
91 fvres ${⊢}{t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\to \left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({t}\right)={F}\left({t}\right)$
92 91 eqcomd ${⊢}{t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\to {F}\left({t}\right)=\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({t}\right)$
93 92 oveq1d ${⊢}{t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\to {F}\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)=\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)$
94 93 adantl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {F}\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)=\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)$
95 94 itgeq2dv ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}{F}\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)d{t}={\int }_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)d{t}$
96 simpl ${⊢}\left({n}={m}\wedge {y}\in ℝ\right)\to {n}={m}$
97 96 oveq2d ${⊢}\left({n}={m}\wedge {y}\in ℝ\right)\to 2{n}=2{m}$
98 97 oveq1d ${⊢}\left({n}={m}\wedge {y}\in ℝ\right)\to 2{n}+1=2{m}+1$
99 98 oveq1d ${⊢}\left({n}={m}\wedge {y}\in ℝ\right)\to \frac{2{n}+1}{2\mathrm{\pi }}=\frac{2{m}+1}{2\mathrm{\pi }}$
100 96 oveq1d ${⊢}\left({n}={m}\wedge {y}\in ℝ\right)\to {n}+\left(\frac{1}{2}\right)={m}+\left(\frac{1}{2}\right)$
101 100 oveq1d ${⊢}\left({n}={m}\wedge {y}\in ℝ\right)\to \left({n}+\left(\frac{1}{2}\right)\right){y}=\left({m}+\left(\frac{1}{2}\right)\right){y}$
102 101 fveq2d ${⊢}\left({n}={m}\wedge {y}\in ℝ\right)\to \mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){y}=\mathrm{sin}\left({m}+\left(\frac{1}{2}\right)\right){y}$
103 102 oveq1d ${⊢}\left({n}={m}\wedge {y}\in ℝ\right)\to \frac{\mathrm{sin}\left({n}+\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){y}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{y}}{2}\right)}$
104 99 103 ifeq12d ${⊢}\left({n}={m}\wedge {y}\in ℝ\right)\to if\left({y}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{n}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){y}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{y}}{2}\right)}\right)=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)$
105 104 mpteq2dva ${⊢}{n}={m}\to \left({y}\in ℝ⟼if\left({y}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{n}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){y}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{y}}{2}\right)}\right)\right)=\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)$
106 105 cbvmptv ${⊢}\left({n}\in ℕ⟼\left({y}\in ℝ⟼if\left({y}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{n}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){y}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{y}}{2}\right)}\right)\right)\right)=\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)$
107 4 106 eqtri ${⊢}{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)$
108 fveq2 ${⊢}{s}={t}\to \left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({s}\right)=\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({t}\right)$
109 oveq1 ${⊢}{s}={t}\to {s}-{X}={t}-{X}$
110 109 fveq2d ${⊢}{s}={t}\to {D}\left({n}\right)\left({s}-{X}\right)={D}\left({n}\right)\left({t}-{X}\right)$
111 108 110 oveq12d ${⊢}{s}={t}\to \left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({s}\right){D}\left({n}\right)\left({s}-{X}\right)=\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)$
112 111 cbvmptv ${⊢}\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({s}\right){D}\left({n}\right)\left({s}-{X}\right)\right)=\left({t}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)\right)$
113 7 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {Q}\in {P}\left({M}\right)$
114 6 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\in ℕ$
115 simpr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}\in ℕ$
116 8 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {X}\in ℝ$
117 50 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right):\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℂ$
118 62 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)↾}_{\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}{⟶}ℂ$
119 64 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {R}\in \left(\left({\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}\right)\right)$
120 66 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {L}\in \left(\left({\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right){lim}_{ℂ}{Q}\left({i}+1\right)\right)$
121 107 5 112 113 114 115 116 117 118 119 120 fourierdlem101 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)d{t}={\int }_{\left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]}\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({X}+{y}\right){D}\left({n}\right)\left({y}\right)d{y}$
122 oveq2 ${⊢}{s}={y}\to {X}+{s}={X}+{y}$
123 122 fveq2d ${⊢}{s}={y}\to {F}\left({X}+{s}\right)={F}\left({X}+{y}\right)$
124 fveq2 ${⊢}{s}={y}\to {D}\left({n}\right)\left({s}\right)={D}\left({n}\right)\left({y}\right)$
125 123 124 oveq12d ${⊢}{s}={y}\to {F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)={F}\left({X}+{y}\right){D}\left({n}\right)\left({y}\right)$
126 125 cbvitgv ${⊢}{\int }_{\left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}={\int }_{\left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)}{F}\left({X}+{y}\right){D}\left({n}\right)\left({y}\right)d{y}$
127 126 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{\left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}={\int }_{\left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)}{F}\left({X}+{y}\right){D}\left({n}\right)\left({y}\right)d{y}$
128 39 a1i ${⊢}{\phi }\to -\mathrm{\pi }\in ℝ$
129 128 8 resubcld ${⊢}{\phi }\to -\mathrm{\pi }-{X}\in ℝ$
130 129 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to -\mathrm{\pi }-{X}\in ℝ$
131 38 a1i ${⊢}{\phi }\to \mathrm{\pi }\in ℝ$
132 131 8 resubcld ${⊢}{\phi }\to \mathrm{\pi }-{X}\in ℝ$
133 132 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \mathrm{\pi }-{X}\in ℝ$
134 49 adantr ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {F}:ℝ⟶ℂ$
135 8 adantr ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {X}\in ℝ$
136 simpr ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]$
137 129 adantr ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to -\mathrm{\pi }-{X}\in ℝ$
138 132 adantr ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to \mathrm{\pi }-{X}\in ℝ$
139 elicc2 ${⊢}\left(-\mathrm{\pi }-{X}\in ℝ\wedge \mathrm{\pi }-{X}\in ℝ\right)\to \left({y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]↔\left({y}\in ℝ\wedge -\mathrm{\pi }-{X}\le {y}\wedge {y}\le \mathrm{\pi }-{X}\right)\right)$
140 137 138 139 syl2anc ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to \left({y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]↔\left({y}\in ℝ\wedge -\mathrm{\pi }-{X}\le {y}\wedge {y}\le \mathrm{\pi }-{X}\right)\right)$
141 136 140 mpbid ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to \left({y}\in ℝ\wedge -\mathrm{\pi }-{X}\le {y}\wedge {y}\le \mathrm{\pi }-{X}\right)$
142 141 simp1d ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {y}\in ℝ$
143 135 142 readdcld ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {X}+{y}\in ℝ$
144 134 143 ffvelrnd ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {F}\left({X}+{y}\right)\in ℂ$
145 144 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {F}\left({X}+{y}\right)\in ℂ$
146 82 ad2antlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {D}\left({n}\right):ℝ⟶ℝ$
147 142 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {y}\in ℝ$
148 146 147 ffvelrnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {D}\left({n}\right)\left({y}\right)\in ℝ$
149 148 recnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {D}\left({n}\right)\left({y}\right)\in ℂ$
150 145 149 mulcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {F}\left({X}+{y}\right){D}\left({n}\right)\left({y}\right)\in ℂ$
151 130 133 150 itgioo ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{\left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)}{F}\left({X}+{y}\right){D}\left({n}\right)\left({y}\right)d{y}={\int }_{\left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]}{F}\left({X}+{y}\right){D}\left({n}\right)\left({y}\right)d{y}$
152 39 a1i ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to -\mathrm{\pi }\in ℝ$
153 38 a1i ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to \mathrm{\pi }\in ℝ$
154 8 recnd ${⊢}{\phi }\to {X}\in ℂ$
155 131 recnd ${⊢}{\phi }\to \mathrm{\pi }\in ℂ$
156 155 negcld ${⊢}{\phi }\to -\mathrm{\pi }\in ℂ$
157 154 156 pncan3d ${⊢}{\phi }\to {X}+\left(-\mathrm{\pi }\right)-{X}=-\mathrm{\pi }$
158 157 eqcomd ${⊢}{\phi }\to -\mathrm{\pi }={X}+\left(-\mathrm{\pi }\right)-{X}$
159 158 adantr ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to -\mathrm{\pi }={X}+\left(-\mathrm{\pi }\right)-{X}$
160 141 simp2d ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to -\mathrm{\pi }-{X}\le {y}$
161 137 142 135 160 leadd2dd ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {X}+\left(-\mathrm{\pi }\right)-{X}\le {X}+{y}$
162 159 161 eqbrtrd ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to -\mathrm{\pi }\le {X}+{y}$
163 141 simp3d ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {y}\le \mathrm{\pi }-{X}$
164 142 138 135 163 leadd2dd ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {X}+{y}\le {X}+\mathrm{\pi }-{X}$
165 154 adantr ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {X}\in ℂ$
166 155 adantr ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to \mathrm{\pi }\in ℂ$
167 165 166 pncan3d ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {X}+\mathrm{\pi }-{X}=\mathrm{\pi }$
168 164 167 breqtrd ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {X}+{y}\le \mathrm{\pi }$
169 152 153 143 162 168 eliccd ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {X}+{y}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]$
170 fvres ${⊢}{X}+{y}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\to \left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({X}+{y}\right)={F}\left({X}+{y}\right)$
171 169 170 syl ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to \left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({X}+{y}\right)={F}\left({X}+{y}\right)$
172 171 eqcomd ${⊢}\left({\phi }\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {F}\left({X}+{y}\right)=\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({X}+{y}\right)$
173 172 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {F}\left({X}+{y}\right)=\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({X}+{y}\right)$
174 173 oveq1d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {y}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {F}\left({X}+{y}\right){D}\left({n}\right)\left({y}\right)=\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({X}+{y}\right){D}\left({n}\right)\left({y}\right)$
175 174 itgeq2dv ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{\left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]}{F}\left({X}+{y}\right){D}\left({n}\right)\left({y}\right)d{y}={\int }_{\left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]}\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({X}+{y}\right){D}\left({n}\right)\left({y}\right)d{y}$
176 127 151 175 3eqtrrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{\left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]}\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({X}+{y}\right){D}\left({n}\right)\left({y}\right)d{y}={\int }_{\left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}$
177 121 176 eqtrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\left({{F}↾}_{\left[-\mathrm{\pi },\mathrm{\pi }\right]}\right)\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)d{t}={\int }_{\left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}$
178 90 95 177 3eqtrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({t}\right){D}\left({n}\right)\left({t}-{X}\right)d{t}={\int }_{\left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}$
179 elioore ${⊢}{s}\in \left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)\to {s}\in ℝ$
180 179 adantl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)\right)\to {s}\in ℝ$
181 49 adantr ${⊢}\left({\phi }\wedge {s}\in \left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)\right)\to {F}:ℝ⟶ℂ$
182 8 adantr ${⊢}\left({\phi }\wedge {s}\in \left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)\right)\to {X}\in ℝ$
183 179 adantl ${⊢}\left({\phi }\wedge {s}\in \left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)\right)\to {s}\in ℝ$
184 182 183 readdcld ${⊢}\left({\phi }\wedge {s}\in \left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)\right)\to {X}+{s}\in ℝ$
185 181 184 ffvelrnd ${⊢}\left({\phi }\wedge {s}\in \left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)\right)\to {F}\left({X}+{s}\right)\in ℂ$
186 185 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)\right)\to {F}\left({X}+{s}\right)\in ℂ$
187 82 ad2antlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)\right)\to {D}\left({n}\right):ℝ⟶ℝ$
188 187 180 ffvelrnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)\right)\to {D}\left({n}\right)\left({s}\right)\in ℝ$
189 188 recnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)\right)\to {D}\left({n}\right)\left({s}\right)\in ℂ$
190 186 189 mulcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)\right)\to {F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\in ℂ$
191 oveq2 ${⊢}{x}={s}\to {X}+{x}={X}+{s}$
192 191 fveq2d ${⊢}{x}={s}\to {F}\left({X}+{x}\right)={F}\left({X}+{s}\right)$
193 fveq2 ${⊢}{x}={s}\to {D}\left({n}\right)\left({x}\right)={D}\left({n}\right)\left({s}\right)$
194 192 193 oveq12d ${⊢}{x}={s}\to {F}\left({X}+{x}\right){D}\left({n}\right)\left({x}\right)={F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)$
195 194 cbvmptv ${⊢}\left({x}\in ℝ⟼{F}\left({X}+{x}\right){D}\left({n}\right)\left({x}\right)\right)=\left({s}\in ℝ⟼{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\right)$
196 11 195 eqtri ${⊢}{G}=\left({s}\in ℝ⟼{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\right)$
197 196 fvmpt2 ${⊢}\left({s}\in ℝ\wedge {F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\in ℂ\right)\to {G}\left({s}\right)={F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)$
198 180 190 197 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)\right)\to {G}\left({s}\right)={F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)$
199 198 eqcomd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)\right)\to {F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)={G}\left({s}\right)$
200 199 itgeq2dv ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{\left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}={\int }_{\left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)}{G}\left({s}\right)d{s}$
201 49 adantr ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}:ℝ⟶ℂ$
202 8 adantr ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {X}\in ℝ$
203 simpr ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {x}\in ℝ$
204 202 203 readdcld ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {X}+{x}\in ℝ$
205 201 204 ffvelrnd ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({X}+{x}\right)\in ℂ$
206 205 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {F}\left({X}+{x}\right)\in ℂ$
207 82 adantl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {D}\left({n}\right):ℝ⟶ℝ$
208 207 ffvelrnda ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {D}\left({n}\right)\left({x}\right)\in ℝ$
209 208 recnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {D}\left({n}\right)\left({x}\right)\in ℂ$
210 206 209 mulcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {F}\left({X}+{x}\right){D}\left({n}\right)\left({x}\right)\in ℂ$
211 210 11 fmptd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {G}:ℝ⟶ℂ$
212 211 adantr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {G}:ℝ⟶ℂ$
213 129 adantr ${⊢}\left({\phi }\wedge {s}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to -\mathrm{\pi }-{X}\in ℝ$
214 132 adantr ${⊢}\left({\phi }\wedge {s}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to \mathrm{\pi }-{X}\in ℝ$
215 simpr ${⊢}\left({\phi }\wedge {s}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {s}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]$
216 eliccre ${⊢}\left(-\mathrm{\pi }-{X}\in ℝ\wedge \mathrm{\pi }-{X}\in ℝ\wedge {s}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {s}\in ℝ$
217 213 214 215 216 syl3anc ${⊢}\left({\phi }\wedge {s}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {s}\in ℝ$
218 217 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {s}\in ℝ$
219 212 218 ffvelrnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]\right)\to {G}\left({s}\right)\in ℂ$
220 130 133 219 itgioo ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{\left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)}{G}\left({s}\right)d{s}={\int }_{\left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]}{G}\left({s}\right)d{s}$
221 fveq2 ${⊢}{s}={x}\to {G}\left({s}\right)={G}\left({x}\right)$
222 221 cbvitgv ${⊢}{\int }_{\left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]}{G}\left({s}\right)d{s}={\int }_{\left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]}{G}\left({x}\right)d{x}$
223 220 222 syl6eq ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{\left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)}{G}\left({s}\right)d{s}={\int }_{\left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]}{G}\left({x}\right)d{x}$
224 200 223 eqtrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{\left(-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right)}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}={\int }_{\left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]}{G}\left({x}\right)d{x}$
225 eqid ${⊢}\mathrm{\pi }-{X}-\left(-\mathrm{\pi }-{X}\right)=\mathrm{\pi }-{X}-\left(-\mathrm{\pi }-{X}\right)$
226 116 renegcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to -{X}\in ℝ$
227 5 fourierdlem2 ${⊢}{M}\in ℕ\to \left({Q}\in {P}\left({M}\right)↔\left({Q}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)\wedge \left(\left({Q}\left(0\right)=-\mathrm{\pi }\wedge {Q}\left({M}\right)=\mathrm{\pi }\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)<{Q}\left({i}+1\right)\right)\right)\right)$
228 6 227 syl ${⊢}{\phi }\to \left({Q}\in {P}\left({M}\right)↔\left({Q}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)\wedge \left(\left({Q}\left(0\right)=-\mathrm{\pi }\wedge {Q}\left({M}\right)=\mathrm{\pi }\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)<{Q}\left({i}+1\right)\right)\right)\right)$
229 7 228 mpbid ${⊢}{\phi }\to \left({Q}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)\wedge \left(\left({Q}\left(0\right)=-\mathrm{\pi }\wedge {Q}\left({M}\right)=\mathrm{\pi }\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)<{Q}\left({i}+1\right)\right)\right)$
230 229 simpld ${⊢}{\phi }\to {Q}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)$
231 elmapi ${⊢}{Q}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)\to {Q}:\left(0\dots {M}\right)⟶ℝ$
232 230 231 syl ${⊢}{\phi }\to {Q}:\left(0\dots {M}\right)⟶ℝ$
233 232 ffvelrnda ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {Q}\left({i}\right)\in ℝ$
234 8 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {X}\in ℝ$
235 233 234 resubcld ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {Q}\left({i}\right)-{X}\in ℝ$
236 235 17 fmptd ${⊢}{\phi }\to {W}:\left(0\dots {M}\right)⟶ℝ$
237 reex ${⊢}ℝ\in \mathrm{V}$
238 ovex ${⊢}\left(0\dots {M}\right)\in \mathrm{V}$
239 237 238 pm3.2i ${⊢}\left(ℝ\in \mathrm{V}\wedge \left(0\dots {M}\right)\in \mathrm{V}\right)$
240 elmapg ${⊢}\left(ℝ\in \mathrm{V}\wedge \left(0\dots {M}\right)\in \mathrm{V}\right)\to \left({W}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)↔{W}:\left(0\dots {M}\right)⟶ℝ\right)$
241 239 240 mp1i ${⊢}{\phi }\to \left({W}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)↔{W}:\left(0\dots {M}\right)⟶ℝ\right)$
242 236 241 mpbird ${⊢}{\phi }\to {W}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)$
243 17 a1i ${⊢}{\phi }\to {W}=\left({i}\in \left(0\dots {M}\right)⟼{Q}\left({i}\right)-{X}\right)$
244 fveq2 ${⊢}{i}=0\to {Q}\left({i}\right)={Q}\left(0\right)$
245 229 simprd ${⊢}{\phi }\to \left(\left({Q}\left(0\right)=-\mathrm{\pi }\wedge {Q}\left({M}\right)=\mathrm{\pi }\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)<{Q}\left({i}+1\right)\right)$
246 245 simpld ${⊢}{\phi }\to \left({Q}\left(0\right)=-\mathrm{\pi }\wedge {Q}\left({M}\right)=\mathrm{\pi }\right)$
247 246 simpld ${⊢}{\phi }\to {Q}\left(0\right)=-\mathrm{\pi }$
248 244 247 sylan9eqr ${⊢}\left({\phi }\wedge {i}=0\right)\to {Q}\left({i}\right)=-\mathrm{\pi }$
249 248 oveq1d ${⊢}\left({\phi }\wedge {i}=0\right)\to {Q}\left({i}\right)-{X}=-\mathrm{\pi }-{X}$
250 0zd ${⊢}{\phi }\to 0\in ℤ$
251 6 nnzd ${⊢}{\phi }\to {M}\in ℤ$
252 0red ${⊢}{M}\in ℕ\to 0\in ℝ$
253 nnre ${⊢}{M}\in ℕ\to {M}\in ℝ$
254 nngt0 ${⊢}{M}\in ℕ\to 0<{M}$
255 252 253 254 ltled ${⊢}{M}\in ℕ\to 0\le {M}$
256 6 255 syl ${⊢}{\phi }\to 0\le {M}$
257 eluz2 ${⊢}{M}\in {ℤ}_{\ge 0}↔\left(0\in ℤ\wedge {M}\in ℤ\wedge 0\le {M}\right)$
258 250 251 256 257 syl3anbrc ${⊢}{\phi }\to {M}\in {ℤ}_{\ge 0}$
259 eluzfz1 ${⊢}{M}\in {ℤ}_{\ge 0}\to 0\in \left(0\dots {M}\right)$
260 258 259 syl ${⊢}{\phi }\to 0\in \left(0\dots {M}\right)$
261 243 249 260 129 fvmptd ${⊢}{\phi }\to {W}\left(0\right)=-\mathrm{\pi }-{X}$
262 fveq2 ${⊢}{i}={M}\to {Q}\left({i}\right)={Q}\left({M}\right)$
263 246 simprd ${⊢}{\phi }\to {Q}\left({M}\right)=\mathrm{\pi }$
264 262 263 sylan9eqr ${⊢}\left({\phi }\wedge {i}={M}\right)\to {Q}\left({i}\right)=\mathrm{\pi }$
265 264 oveq1d ${⊢}\left({\phi }\wedge {i}={M}\right)\to {Q}\left({i}\right)-{X}=\mathrm{\pi }-{X}$
266 eluzfz2 ${⊢}{M}\in {ℤ}_{\ge 0}\to {M}\in \left(0\dots {M}\right)$
267 258 266 syl ${⊢}{\phi }\to {M}\in \left(0\dots {M}\right)$
268 243 265 267 132 fvmptd ${⊢}{\phi }\to {W}\left({M}\right)=\mathrm{\pi }-{X}$
269 261 268 jca ${⊢}{\phi }\to \left({W}\left(0\right)=-\mathrm{\pi }-{X}\wedge {W}\left({M}\right)=\mathrm{\pi }-{X}\right)$
270 232 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}:\left(0\dots {M}\right)⟶ℝ$
271 elfzofz ${⊢}{i}\in \left(0..^{M}\right)\to {i}\in \left(0\dots {M}\right)$
272 271 adantl ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {i}\in \left(0\dots {M}\right)$
273 270 272 ffvelrnd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}\right)\in ℝ$
274 fzofzp1 ${⊢}{i}\in \left(0..^{M}\right)\to {i}+1\in \left(0\dots {M}\right)$
275 274 adantl ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {i}+1\in \left(0\dots {M}\right)$
276 270 275 ffvelrnd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}+1\right)\in ℝ$
277 8 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {X}\in ℝ$
278 245 simprd ${⊢}{\phi }\to \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{Q}\left({i}\right)<{Q}\left({i}+1\right)$
279 278 r19.21bi ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}\right)<{Q}\left({i}+1\right)$
280 273 276 277 279 ltsub1dd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}\right)-{X}<{Q}\left({i}+1\right)-{X}$
281 272 235 syldan ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}\right)-{X}\in ℝ$
282 17 fvmpt2 ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge {Q}\left({i}\right)-{X}\in ℝ\right)\to {W}\left({i}\right)={Q}\left({i}\right)-{X}$
283 272 281 282 syl2anc ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}\right)={Q}\left({i}\right)-{X}$
284 fveq2 ${⊢}{i}={j}\to {Q}\left({i}\right)={Q}\left({j}\right)$
285 284 oveq1d ${⊢}{i}={j}\to {Q}\left({i}\right)-{X}={Q}\left({j}\right)-{X}$
286 285 cbvmptv ${⊢}\left({i}\in \left(0\dots {M}\right)⟼{Q}\left({i}\right)-{X}\right)=\left({j}\in \left(0\dots {M}\right)⟼{Q}\left({j}\right)-{X}\right)$
287 17 286 eqtri ${⊢}{W}=\left({j}\in \left(0\dots {M}\right)⟼{Q}\left({j}\right)-{X}\right)$
288 287 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}=\left({j}\in \left(0\dots {M}\right)⟼{Q}\left({j}\right)-{X}\right)$
289 fveq2 ${⊢}{j}={i}+1\to {Q}\left({j}\right)={Q}\left({i}+1\right)$
290 289 oveq1d ${⊢}{j}={i}+1\to {Q}\left({j}\right)-{X}={Q}\left({i}+1\right)-{X}$
291 290 adantl ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {j}={i}+1\right)\to {Q}\left({j}\right)-{X}={Q}\left({i}+1\right)-{X}$
292 276 277 resubcld ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}+1\right)-{X}\in ℝ$
293 288 291 275 292 fvmptd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}+1\right)={Q}\left({i}+1\right)-{X}$
294 280 283 293 3brtr4d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}\right)<{W}\left({i}+1\right)$
295 294 ralrimiva ${⊢}{\phi }\to \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)<{W}\left({i}+1\right)$
296 242 269 295 jca32 ${⊢}{\phi }\to \left({W}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)\wedge \left(\left({W}\left(0\right)=-\mathrm{\pi }-{X}\wedge {W}\left({M}\right)=\mathrm{\pi }-{X}\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)<{W}\left({i}+1\right)\right)\right)$
297 16 fourierdlem2 ${⊢}{M}\in ℕ\to \left({W}\in {O}\left({M}\right)↔\left({W}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)\wedge \left(\left({W}\left(0\right)=-\mathrm{\pi }-{X}\wedge {W}\left({M}\right)=\mathrm{\pi }-{X}\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)<{W}\left({i}+1\right)\right)\right)\right)$
298 6 297 syl ${⊢}{\phi }\to \left({W}\in {O}\left({M}\right)↔\left({W}\in \left({ℝ}^{\left(0\dots {M}\right)}\right)\wedge \left(\left({W}\left(0\right)=-\mathrm{\pi }-{X}\wedge {W}\left({M}\right)=\mathrm{\pi }-{X}\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{W}\left({i}\right)<{W}\left({i}+1\right)\right)\right)\right)$
299 296 298 mpbird ${⊢}{\phi }\to {W}\in {O}\left({M}\right)$
300 299 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {W}\in {O}\left({M}\right)$
301 155 156 154 nnncan2d ${⊢}{\phi }\to \mathrm{\pi }-{X}-\left(-\mathrm{\pi }-{X}\right)=\mathrm{\pi }-\left(-\mathrm{\pi }\right)$
302 picn ${⊢}\mathrm{\pi }\in ℂ$
303 302 2timesi ${⊢}2\mathrm{\pi }=\mathrm{\pi }+\mathrm{\pi }$
304 302 302 subnegi ${⊢}\mathrm{\pi }-\left(-\mathrm{\pi }\right)=\mathrm{\pi }+\mathrm{\pi }$
305 303 15 304 3eqtr4i ${⊢}{T}=\mathrm{\pi }-\left(-\mathrm{\pi }\right)$
306 301 305 syl6eqr ${⊢}{\phi }\to \mathrm{\pi }-{X}-\left(-\mathrm{\pi }-{X}\right)={T}$
307 306 oveq2d ${⊢}{\phi }\to {x}+\left(\mathrm{\pi }-{X}\right)-\left(-\mathrm{\pi }-{X}\right)={x}+{T}$
308 307 fveq2d ${⊢}{\phi }\to {G}\left({x}+\left(\mathrm{\pi }-{X}\right)-\left(-\mathrm{\pi }-{X}\right)\right)={G}\left({x}+{T}\right)$
309 308 ad2antrr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {G}\left({x}+\left(\mathrm{\pi }-{X}\right)-\left(-\mathrm{\pi }-{X}\right)\right)={G}\left({x}+{T}\right)$
310 simpr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {x}\in ℝ$
311 11 fvmpt2 ${⊢}\left({x}\in ℝ\wedge {F}\left({X}+{x}\right){D}\left({n}\right)\left({x}\right)\in ℂ\right)\to {G}\left({x}\right)={F}\left({X}+{x}\right){D}\left({n}\right)\left({x}\right)$
312 310 210 311 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {G}\left({x}\right)={F}\left({X}+{x}\right){D}\left({n}\right)\left({x}\right)$
313 154 adantr ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {X}\in ℂ$
314 203 recnd ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {x}\in ℂ$
315 2re ${⊢}2\in ℝ$
316 315 38 remulcli ${⊢}2\mathrm{\pi }\in ℝ$
317 15 316 eqeltri ${⊢}{T}\in ℝ$
318 317 a1i ${⊢}{\phi }\to {T}\in ℝ$
319 318 recnd ${⊢}{\phi }\to {T}\in ℂ$
320 319 adantr ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {T}\in ℂ$
321 313 314 320 addassd ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {X}+{x}+{T}={X}+{x}+{T}$
322 321 eqcomd ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {X}+{x}+{T}={X}+{x}+{T}$
323 322 fveq2d ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({X}+{x}+{T}\right)={F}\left({X}+{x}+{T}\right)$
324 simpl ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {\phi }$
325 324 204 jca ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({\phi }\wedge {X}+{x}\in ℝ\right)$
326 eleq1 ${⊢}{s}={X}+{x}\to \left({s}\in ℝ↔{X}+{x}\in ℝ\right)$
327 326 anbi2d ${⊢}{s}={X}+{x}\to \left(\left({\phi }\wedge {s}\in ℝ\right)↔\left({\phi }\wedge {X}+{x}\in ℝ\right)\right)$
328 oveq1 ${⊢}{s}={X}+{x}\to {s}+{T}={X}+{x}+{T}$
329 328 fveq2d ${⊢}{s}={X}+{x}\to {F}\left({s}+{T}\right)={F}\left({X}+{x}+{T}\right)$
330 fveq2 ${⊢}{s}={X}+{x}\to {F}\left({s}\right)={F}\left({X}+{x}\right)$
331 329 330 eqeq12d ${⊢}{s}={X}+{x}\to \left({F}\left({s}+{T}\right)={F}\left({s}\right)↔{F}\left({X}+{x}+{T}\right)={F}\left({X}+{x}\right)\right)$
332 327 331 imbi12d ${⊢}{s}={X}+{x}\to \left(\left(\left({\phi }\wedge {s}\in ℝ\right)\to {F}\left({s}+{T}\right)={F}\left({s}\right)\right)↔\left(\left({\phi }\wedge {X}+{x}\in ℝ\right)\to {F}\left({X}+{x}+{T}\right)={F}\left({X}+{x}\right)\right)\right)$
333 eleq1 ${⊢}{x}={s}\to \left({x}\in ℝ↔{s}\in ℝ\right)$
334 333 anbi2d ${⊢}{x}={s}\to \left(\left({\phi }\wedge {x}\in ℝ\right)↔\left({\phi }\wedge {s}\in ℝ\right)\right)$
335 oveq1 ${⊢}{x}={s}\to {x}+{T}={s}+{T}$
336 335 fveq2d ${⊢}{x}={s}\to {F}\left({x}+{T}\right)={F}\left({s}+{T}\right)$
337 fveq2 ${⊢}{x}={s}\to {F}\left({x}\right)={F}\left({s}\right)$
338 336 337 eqeq12d ${⊢}{x}={s}\to \left({F}\left({x}+{T}\right)={F}\left({x}\right)↔{F}\left({s}+{T}\right)={F}\left({s}\right)\right)$
339 334 338 imbi12d ${⊢}{x}={s}\to \left(\left(\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)\right)↔\left(\left({\phi }\wedge {s}\in ℝ\right)\to {F}\left({s}+{T}\right)={F}\left({s}\right)\right)\right)$
340 339 10 chvarvv ${⊢}\left({\phi }\wedge {s}\in ℝ\right)\to {F}\left({s}+{T}\right)={F}\left({s}\right)$
341 332 340 vtoclg ${⊢}{X}+{x}\in ℝ\to \left(\left({\phi }\wedge {X}+{x}\in ℝ\right)\to {F}\left({X}+{x}+{T}\right)={F}\left({X}+{x}\right)\right)$
342 204 325 341 sylc ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({X}+{x}+{T}\right)={F}\left({X}+{x}\right)$
343 323 342 eqtr2d ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({X}+{x}\right)={F}\left({X}+{x}+{T}\right)$
344 343 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {F}\left({X}+{x}\right)={F}\left({X}+{x}+{T}\right)$
345 4 15 dirkerper ${⊢}\left({n}\in ℕ\wedge {x}\in ℝ\right)\to {D}\left({n}\right)\left({x}+{T}\right)={D}\left({n}\right)\left({x}\right)$
346 345 eqcomd ${⊢}\left({n}\in ℕ\wedge {x}\in ℝ\right)\to {D}\left({n}\right)\left({x}\right)={D}\left({n}\right)\left({x}+{T}\right)$
347 346 adantll ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {D}\left({n}\right)\left({x}\right)={D}\left({n}\right)\left({x}+{T}\right)$
348 344 347 oveq12d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {F}\left({X}+{x}\right){D}\left({n}\right)\left({x}\right)={F}\left({X}+{x}+{T}\right){D}\left({n}\right)\left({x}+{T}\right)$
349 196 a1i ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {G}=\left({s}\in ℝ⟼{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\right)$
350 oveq2 ${⊢}{s}={x}+{T}\to {X}+{s}={X}+{x}+{T}$
351 350 fveq2d ${⊢}{s}={x}+{T}\to {F}\left({X}+{s}\right)={F}\left({X}+{x}+{T}\right)$
352 fveq2 ${⊢}{s}={x}+{T}\to {D}\left({n}\right)\left({s}\right)={D}\left({n}\right)\left({x}+{T}\right)$
353 351 352 oveq12d ${⊢}{s}={x}+{T}\to {F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)={F}\left({X}+{x}+{T}\right){D}\left({n}\right)\left({x}+{T}\right)$
354 353 adantl ${⊢}\left(\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\wedge {s}={x}+{T}\right)\to {F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)={F}\left({X}+{x}+{T}\right){D}\left({n}\right)\left({x}+{T}\right)$
355 317 a1i ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {T}\in ℝ$
356 310 355 readdcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {x}+{T}\in ℝ$
357 317 a1i ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {T}\in ℝ$
358 203 357 readdcld ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {x}+{T}\in ℝ$
359 202 358 readdcld ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {X}+{x}+{T}\in ℝ$
360 201 359 ffvelrnd ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({X}+{x}+{T}\right)\in ℂ$
361 360 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {F}\left({X}+{x}+{T}\right)\in ℂ$
362 82 ad2antlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {D}\left({n}\right):ℝ⟶ℝ$
363 362 356 ffvelrnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {D}\left({n}\right)\left({x}+{T}\right)\in ℝ$
364 363 recnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {D}\left({n}\right)\left({x}+{T}\right)\in ℂ$
365 361 364 mulcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {F}\left({X}+{x}+{T}\right){D}\left({n}\right)\left({x}+{T}\right)\in ℂ$
366 349 354 356 365 fvmptd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {G}\left({x}+{T}\right)={F}\left({X}+{x}+{T}\right){D}\left({n}\right)\left({x}+{T}\right)$
367 366 eqcomd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {F}\left({X}+{x}+{T}\right){D}\left({n}\right)\left({x}+{T}\right)={G}\left({x}+{T}\right)$
368 312 348 367 3eqtrrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {G}\left({x}+{T}\right)={G}\left({x}\right)$
369 309 368 eqtrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {x}\in ℝ\right)\to {G}\left({x}+\left(\mathrm{\pi }-{X}\right)-\left(-\mathrm{\pi }-{X}\right)\right)={G}\left({x}\right)$
370 196 reseq1i ${⊢}{{G}↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}={\left({s}\in ℝ⟼{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}$
371 370 a1i ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {{G}↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}={\left({s}\in ℝ⟼{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}$
372 ioossre ${⊢}\left({W}\left({i}\right),{W}\left({i}+1\right)\right)\subseteq ℝ$
373 resmpt ${⊢}\left({W}\left({i}\right),{W}\left({i}+1\right)\right)\subseteq ℝ\to {\left({s}\in ℝ⟼{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}=\left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\right)$
374 372 373 ax-mp ${⊢}{\left({s}\in ℝ⟼{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}=\left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\right)$
375 371 374 syl6eq ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {{G}↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}=\left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\right)$
376 273 rexrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}\right)\in {ℝ}^{*}$
377 376 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {Q}\left({i}\right)\in {ℝ}^{*}$
378 276 rexrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}+1\right)\in {ℝ}^{*}$
379 378 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {Q}\left({i}+1\right)\in {ℝ}^{*}$
380 8 adantr ${⊢}\left({\phi }\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}\in ℝ$
381 elioore ${⊢}{s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\to {s}\in ℝ$
382 381 adantl ${⊢}\left({\phi }\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {s}\in ℝ$
383 380 382 readdcld ${⊢}\left({\phi }\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{s}\in ℝ$
384 383 adantlr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{s}\in ℝ$
385 eleq1 ${⊢}{x}={s}\to \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)↔{s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)$
386 385 anbi2d ${⊢}{x}={s}\to \left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)↔\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\right)$
387 191 breq2d ${⊢}{x}={s}\to \left({Q}\left({i}\right)<{X}+{x}↔{Q}\left({i}\right)<{X}+{s}\right)$
388 386 387 imbi12d ${⊢}{x}={s}\to \left(\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {Q}\left({i}\right)<{X}+{x}\right)↔\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {Q}\left({i}\right)<{X}+{s}\right)\right)$
389 154 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {X}\in ℂ$
390 283 281 eqeltrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}\right)\in ℝ$
391 390 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}\right)\in ℂ$
392 389 391 addcomd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {X}+{W}\left({i}\right)={W}\left({i}\right)+{X}$
393 283 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}\right)+{X}={Q}\left({i}\right)-{X}+{X}$
394 273 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}\right)\in ℂ$
395 394 389 npcand ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}\right)-{X}+{X}={Q}\left({i}\right)$
396 392 393 395 3eqtrrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}\right)={X}+{W}\left({i}\right)$
397 396 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {Q}\left({i}\right)={X}+{W}\left({i}\right)$
398 390 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {W}\left({i}\right)\in ℝ$
399 elioore ${⊢}{x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\to {x}\in ℝ$
400 399 adantl ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {x}\in ℝ$
401 8 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}\in ℝ$
402 390 rexrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}\right)\in {ℝ}^{*}$
403 402 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {W}\left({i}\right)\in {ℝ}^{*}$
404 293 292 eqeltrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}+1\right)\in ℝ$
405 404 rexrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}+1\right)\in {ℝ}^{*}$
406 405 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {W}\left({i}+1\right)\in {ℝ}^{*}$
407 simpr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)$
408 ioogtlb ${⊢}\left({W}\left({i}\right)\in {ℝ}^{*}\wedge {W}\left({i}+1\right)\in {ℝ}^{*}\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {W}\left({i}\right)<{x}$
409 403 406 407 408 syl3anc ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {W}\left({i}\right)<{x}$
410 398 400 401 409 ltadd2dd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{W}\left({i}\right)<{X}+{x}$
411 397 410 eqbrtrd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {Q}\left({i}\right)<{X}+{x}$
412 388 411 chvarvv ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {Q}\left({i}\right)<{X}+{s}$
413 191 breq1d ${⊢}{x}={s}\to \left({X}+{x}<{Q}\left({i}+1\right)↔{X}+{s}<{Q}\left({i}+1\right)\right)$
414 386 413 imbi12d ${⊢}{x}={s}\to \left(\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{x}<{Q}\left({i}+1\right)\right)↔\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{s}<{Q}\left({i}+1\right)\right)\right)$
415 404 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {W}\left({i}+1\right)\in ℝ$
416 iooltub ${⊢}\left({W}\left({i}\right)\in {ℝ}^{*}\wedge {W}\left({i}+1\right)\in {ℝ}^{*}\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {x}<{W}\left({i}+1\right)$
417 403 406 407 416 syl3anc ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {x}<{W}\left({i}+1\right)$
418 400 415 401 417 ltadd2dd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{x}<{X}+{W}\left({i}+1\right)$
419 404 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}+1\right)\in ℂ$
420 389 419 addcomd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {X}+{W}\left({i}+1\right)={W}\left({i}+1\right)+{X}$
421 293 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}+1\right)+{X}={Q}\left({i}+1\right)-{X}+{X}$
422 276 recnd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}+1\right)\in ℂ$
423 422 389 npcand ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}+1\right)-{X}+{X}={Q}\left({i}+1\right)$
424 420 421 423 3eqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {X}+{W}\left({i}+1\right)={Q}\left({i}+1\right)$
425 424 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{W}\left({i}+1\right)={Q}\left({i}+1\right)$
426 418 425 breqtrd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{x}<{Q}\left({i}+1\right)$
427 414 426 chvarvv ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{s}<{Q}\left({i}+1\right)$
428 377 379 384 412 427 eliood ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{s}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)$
429 191 cbvmptv ${⊢}\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)=\left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{s}\right)$
430 429 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)=\left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{s}\right)$
431 ioossre ${⊢}\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\subseteq ℝ$
432 431 a1i ${⊢}{\phi }\to \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\subseteq ℝ$
433 9 432 feqresmpt ${⊢}{\phi }\to {{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}=\left({x}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{F}\left({x}\right)\right)$
434 433 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}=\left({x}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)⟼{F}\left({x}\right)\right)$
435 fveq2 ${⊢}{x}={X}+{s}\to {F}\left({x}\right)={F}\left({X}+{s}\right)$
436 428 430 434 435 fmptco ${⊢}\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)\circ \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)=\left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{s}\right)\right)$
437 eqid ${⊢}\left({x}\in ℂ⟼{X}+{x}\right)=\left({x}\in ℂ⟼{X}+{x}\right)$
438 ssid ${⊢}ℂ\subseteq ℂ$
439 438 a1i ${⊢}{\phi }\to ℂ\subseteq ℂ$
440 439 154 439 constcncfg ${⊢}{\phi }\to \left({x}\in ℂ⟼{X}\right):ℂ\underset{cn}{⟶}ℂ$
441 cncfmptid ${⊢}\left(ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left({x}\in ℂ⟼{x}\right):ℂ\underset{cn}{⟶}ℂ$
442 438 438 441 mp2an ${⊢}\left({x}\in ℂ⟼{x}\right):ℂ\underset{cn}{⟶}ℂ$
443 442 a1i ${⊢}{\phi }\to \left({x}\in ℂ⟼{x}\right):ℂ\underset{cn}{⟶}ℂ$
444 440 443 addcncf ${⊢}{\phi }\to \left({x}\in ℂ⟼{X}+{x}\right):ℂ\underset{cn}{⟶}ℂ$
445 444 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in ℂ⟼{X}+{x}\right):ℂ\underset{cn}{⟶}ℂ$
446 ioosscn ${⊢}\left({W}\left({i}\right),{W}\left({i}+1\right)\right)\subseteq ℂ$
447 446 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\subseteq ℂ$
448 ioosscn ${⊢}\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\subseteq ℂ$
449 448 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\subseteq ℂ$
450 376 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {Q}\left({i}\right)\in {ℝ}^{*}$
451 378 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {Q}\left({i}+1\right)\in {ℝ}^{*}$
452 8 adantr ${⊢}\left({\phi }\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}\in ℝ$
453 399 adantl ${⊢}\left({\phi }\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {x}\in ℝ$
454 452 453 readdcld ${⊢}\left({\phi }\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{x}\in ℝ$
455 454 adantlr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{x}\in ℝ$
456 450 451 455 411 426 eliood ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{x}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)$
457 437 445 447 449 456 cncfmptssg ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right):\left({W}\left({i}\right),{W}\left({i}+1\right)\right)\underset{cn}{⟶}\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)$
458 457 12 cncfco ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left(\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\circ \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)\right):\left({W}\left({i}\right),{W}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
459 436 458 eqeltrrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{s}\right)\right):\left({W}\left({i}\right),{W}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
460 459 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{s}\right)\right):\left({W}\left({i}\right),{W}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
461 eqid ${⊢}\left({s}\in ℝ⟼{D}\left({n}\right)\left({s}\right)\right)=\left({s}\in ℝ⟼{D}\left({n}\right)\left({s}\right)\right)$
462 82 feqmptd ${⊢}{n}\in ℕ\to {D}\left({n}\right)=\left({s}\in ℝ⟼{D}\left({n}\right)\left({s}\right)\right)$
463 cncfss
464 47 438 463 mp2an
465 4 dirkercncf ${⊢}{n}\in ℕ\to {D}\left({n}\right):ℝ\underset{cn}{⟶}ℝ$
466 464 465 sseldi ${⊢}{n}\in ℕ\to {D}\left({n}\right):ℝ\underset{cn}{⟶}ℂ$
467 462 466 eqeltrrd ${⊢}{n}\in ℕ\to \left({s}\in ℝ⟼{D}\left({n}\right)\left({s}\right)\right):ℝ\underset{cn}{⟶}ℂ$
468 372 a1i ${⊢}{n}\in ℕ\to \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\subseteq ℝ$
469 438 a1i ${⊢}{n}\in ℕ\to ℂ\subseteq ℂ$
470 cncff ${⊢}{D}\left({n}\right):ℝ\underset{cn}{⟶}ℂ\to {D}\left({n}\right):ℝ⟶ℂ$
471 466 470 syl ${⊢}{n}\in ℕ\to {D}\left({n}\right):ℝ⟶ℂ$
472 471 adantr ${⊢}\left({n}\in ℕ\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {D}\left({n}\right):ℝ⟶ℂ$
473 381 adantl ${⊢}\left({n}\in ℕ\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {s}\in ℝ$
474 472 473 ffvelrnd ${⊢}\left({n}\in ℕ\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {D}\left({n}\right)\left({s}\right)\in ℂ$
475 461 467 468 469 474 cncfmptssg ${⊢}{n}\in ℕ\to \left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{D}\left({n}\right)\left({s}\right)\right):\left({W}\left({i}\right),{W}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
476 475 ad2antlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{D}\left({n}\right)\left({s}\right)\right):\left({W}\left({i}\right),{W}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
477 460 476 mulcncf ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\right):\left({W}\left({i}\right),{W}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
478 375 477 eqeltrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{G}↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right):\left({W}\left({i}\right),{W}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
479 453 205 syldan ${⊢}\left({\phi }\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {F}\left({X}+{x}\right)\in ℂ$
480 479 adantlr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {F}\left({X}+{x}\right)\in ℂ$
481 eqid ${⊢}\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)=\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)$
482 480 481 fmptd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right):\left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟶ℂ$
483 482 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right):\left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟶ℂ$
484 82 ad2antlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {D}\left({n}\right):ℝ⟶ℝ$
485 372 a1i ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\subseteq ℝ$
486 484 485 fssresd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right):\left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟶ℝ$
487 47 a1i ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to ℝ\subseteq ℂ$
488 486 487 fssd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right):\left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟶ℂ$
489 eqid ${⊢}\left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)\left({s}\right)\left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right)\left({s}\right)\right)=\left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)\left({s}\right)\left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right)\left({s}\right)\right)$
490 fdm ${⊢}{F}:ℝ⟶ℂ\to \mathrm{dom}{F}=ℝ$
491 49 490 syl ${⊢}{\phi }\to \mathrm{dom}{F}=ℝ$
492 431 491 sseqtrrid ${⊢}{\phi }\to \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\subseteq \mathrm{dom}{F}$
493 ssdmres ${⊢}\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\subseteq \mathrm{dom}{F}↔\mathrm{dom}\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)$
494 492 493 sylib ${⊢}{\phi }\to \mathrm{dom}\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)$
495 494 eqcomd ${⊢}{\phi }\to \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)=\mathrm{dom}\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)$
496 495 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)=\mathrm{dom}\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)$
497 456 496 eleqtrd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{x}\in \mathrm{dom}\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)$
498 273 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {Q}\left({i}\right)\in ℝ$
499 498 411 gtned ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{x}\ne {Q}\left({i}\right)$
500 eldifsn ${⊢}{X}+{x}\in \left(\mathrm{dom}\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\setminus \left\{{Q}\left({i}\right)\right\}\right)↔\left({X}+{x}\in \mathrm{dom}\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\wedge {X}+{x}\ne {Q}\left({i}\right)\right)$
501 497 499 500 sylanbrc ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{x}\in \left(\mathrm{dom}\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\setminus \left\{{Q}\left({i}\right)\right\}\right)$
502 501 ralrimiva ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \forall {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}{X}+{x}\in \left(\mathrm{dom}\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\setminus \left\{{Q}\left({i}\right)\right\}\right)$
503 eqid ${⊢}\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)=\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)$
504 503 rnmptss ${⊢}\forall {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}{X}+{x}\in \left(\mathrm{dom}\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\setminus \left\{{Q}\left({i}\right)\right\}\right)\to \mathrm{ran}\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)\subseteq \mathrm{dom}\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\setminus \left\{{Q}\left({i}\right)\right\}$
505 502 504 syl ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \mathrm{ran}\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)\subseteq \mathrm{dom}\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\setminus \left\{{Q}\left({i}\right)\right\}$
506 eqidd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)=\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)$
507 oveq2 ${⊢}{x}={W}\left({i}\right)\to {X}+{x}={X}+{W}\left({i}\right)$
508 507 adantl ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}={W}\left({i}\right)\right)\to {X}+{x}={X}+{W}\left({i}\right)$
509 390 leidd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}\right)\le {W}\left({i}\right)$
510 390 404 294 ltled ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}\right)\le {W}\left({i}+1\right)$
511 390 404 390 509 510 eliccd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}\right)\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]$
512 396 273 eqeltrrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {X}+{W}\left({i}\right)\in ℝ$
513 506 508 511 512 fvmptd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)\left({W}\left({i}\right)\right)={X}+{W}\left({i}\right)$
514 396 eqcomd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {X}+{W}\left({i}\right)={Q}\left({i}\right)$
515 513 514 eqtr2d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}\right)=\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)\left({W}\left({i}\right)\right)$
516 390 404 iccssred ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\subseteq ℝ$
517 516 47 sstrdi ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\subseteq ℂ$
518 517 resmptd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {\left({x}\in ℂ⟼{X}+{x}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}=\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)$
519 rescncf ${⊢}\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\subseteq ℂ\to \left(\left({x}\in ℂ⟼{X}+{x}\right):ℂ\underset{cn}{⟶}ℂ\to \left({\left({x}\in ℂ⟼{X}+{x}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right):\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\underset{cn}{⟶}ℂ\right)$
520 517 445 519 sylc ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({\left({x}\in ℂ⟼{X}+{x}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right):\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\underset{cn}{⟶}ℂ$
521 518 520 eqeltrrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right):\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\underset{cn}{⟶}ℂ$
522 521 511 cnlimci ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)\left({W}\left({i}\right)\right)\in \left(\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right){lim}_{ℂ}{W}\left({i}\right)\right)$
523 515 522 eqeltrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}\right)\in \left(\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right){lim}_{ℂ}{W}\left({i}\right)\right)$
524 ioossicc ${⊢}\left({W}\left({i}\right),{W}\left({i}+1\right)\right)\subseteq \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]$
525 resmpt ${⊢}\left({W}\left({i}\right),{W}\left({i}+1\right)\right)\subseteq \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\to {\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}=\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)$
526 524 525 ax-mp ${⊢}{\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}=\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)$
527 526 eqcomi ${⊢}\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)={\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}$
528 527 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)={\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}$
529 528 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right){lim}_{ℂ}{W}\left({i}\right)=\left({\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}\right)$
530 154 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\right)\to {X}\in ℂ$
531 390 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\right)\to {W}\left({i}\right)\in ℝ$
532 404 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\right)\to {W}\left({i}+1\right)\in ℝ$
533 simpr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\right)\to {x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]$
534 eliccre ${⊢}\left({W}\left({i}\right)\in ℝ\wedge {W}\left({i}+1\right)\in ℝ\wedge {x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\right)\to {x}\in ℝ$
535 531 532 533 534 syl3anc ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\right)\to {x}\in ℝ$
536 535 recnd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\right)\to {x}\in ℂ$
537 530 536 addcld ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\right)\to {X}+{x}\in ℂ$
538 eqid ${⊢}\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)=\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)$
539 537 538 fmptd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right):\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟶ℂ$
540 390 404 294 539 limciccioolb ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}\right)=\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right){lim}_{ℂ}{W}\left({i}\right)$
541 529 540 eqtr2d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right){lim}_{ℂ}{W}\left({i}\right)=\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right){lim}_{ℂ}{W}\left({i}\right)$
542 523 541 eleqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}\right)\in \left(\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right){lim}_{ℂ}{W}\left({i}\right)\right)$
543 505 542 13 limccog ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {R}\in \left(\left(\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\circ \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)\right){lim}_{ℂ}{W}\left({i}\right)\right)$
544 49 432 fssresd ${⊢}{\phi }\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)⟶ℂ$
545 544 adantr ${⊢}\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)⟶ℂ$
546 456 503 fmptd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right):\left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟶\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)$
547 fcompt ${⊢}\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)⟶ℂ\wedge \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right):\left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟶\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\right)\to \left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\circ \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)=\left({y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\left(\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)\left({y}\right)\right)\right)$
548 545 546 547 syl2anc ${⊢}\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)\circ \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)=\left({y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\left(\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)\left({y}\right)\right)\right)$
549 eqidd ${⊢}\left({\phi }\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)=\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)$
550 oveq2 ${⊢}{x}={y}\to {X}+{x}={X}+{y}$
551 550 adantl ${⊢}\left(\left({\phi }\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\wedge {x}={y}\right)\to {X}+{x}={X}+{y}$
552 simpr ${⊢}\left({\phi }\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)$
553 8 adantr ${⊢}\left({\phi }\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}\in ℝ$
554 372 552 sseldi ${⊢}\left({\phi }\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {y}\in ℝ$
555 553 554 readdcld ${⊢}\left({\phi }\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{y}\in ℝ$
556 549 551 552 555 fvmptd ${⊢}\left({\phi }\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)\left({y}\right)={X}+{y}$
557 556 fveq2d ${⊢}\left({\phi }\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to \left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\left(\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)\left({y}\right)\right)=\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\left({X}+{y}\right)$
558 557 adantlr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to \left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\left(\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)\left({y}\right)\right)=\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\left({X}+{y}\right)$
559 376 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {Q}\left({i}\right)\in {ℝ}^{*}$
560 378 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {Q}\left({i}+1\right)\in {ℝ}^{*}$
561 555 adantlr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{y}\in ℝ$
562 396 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {Q}\left({i}\right)={X}+{W}\left({i}\right)$
563 390 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {W}\left({i}\right)\in ℝ$
564 554 adantlr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {y}\in ℝ$
565 8 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}\in ℝ$
566 402 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {W}\left({i}\right)\in {ℝ}^{*}$
567 405 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {W}\left({i}+1\right)\in {ℝ}^{*}$
568 simpr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)$
569 ioogtlb ${⊢}\left({W}\left({i}\right)\in {ℝ}^{*}\wedge {W}\left({i}+1\right)\in {ℝ}^{*}\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {W}\left({i}\right)<{y}$
570 566 567 568 569 syl3anc ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {W}\left({i}\right)<{y}$
571 563 564 565 570 ltadd2dd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{W}\left({i}\right)<{X}+{y}$
572 562 571 eqbrtrd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {Q}\left({i}\right)<{X}+{y}$
573 404 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {W}\left({i}+1\right)\in ℝ$
574 iooltub ${⊢}\left({W}\left({i}\right)\in {ℝ}^{*}\wedge {W}\left({i}+1\right)\in {ℝ}^{*}\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {y}<{W}\left({i}+1\right)$
575 566 567 568 574 syl3anc ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {y}<{W}\left({i}+1\right)$
576 564 573 565 575 ltadd2dd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{y}<{X}+{W}\left({i}+1\right)$
577 424 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{W}\left({i}+1\right)={Q}\left({i}+1\right)$
578 576 577 breqtrd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{y}<{Q}\left({i}+1\right)$
579 559 560 561 572 578 eliood ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{y}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)$
580 fvres ${⊢}{X}+{y}\in \left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)\to \left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\left({X}+{y}\right)={F}\left({X}+{y}\right)$
581 579 580 syl ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to \left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\left({X}+{y}\right)={F}\left({X}+{y}\right)$
582 558 581 eqtrd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to \left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\left(\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)\left({y}\right)\right)={F}\left({X}+{y}\right)$
583 582 mpteq2dva ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\left(\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)\left({y}\right)\right)\right)=\left({y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{y}\right)\right)$
584 550 fveq2d ${⊢}{x}={y}\to {F}\left({X}+{x}\right)={F}\left({X}+{y}\right)$
585 584 cbvmptv ${⊢}\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)=\left({y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{y}\right)\right)$
586 583 585 syl6eqr ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({y}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\left(\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)\left({y}\right)\right)\right)=\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)$
587 548 586 eqtrd ${⊢}\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)\circ \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)=\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)$
588 587 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left(\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\circ \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)\right){lim}_{ℂ}{W}\left({i}\right)=\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right){lim}_{ℂ}{W}\left({i}\right)$
589 543 588 eleqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {R}\in \left(\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right){lim}_{ℂ}{W}\left({i}\right)\right)$
590 589 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {R}\in \left(\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right){lim}_{ℂ}{W}\left({i}\right)\right)$
591 fvres ${⊢}{W}\left({i}\right)\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\to \left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)\left({W}\left({i}\right)\right)={D}\left({n}\right)\left({W}\left({i}\right)\right)$
592 511 591 syl ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)\left({W}\left({i}\right)\right)={D}\left({n}\right)\left({W}\left({i}\right)\right)$
593 592 eqcomd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {D}\left({n}\right)\left({W}\left({i}\right)\right)=\left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)\left({W}\left({i}\right)\right)$
594 593 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {D}\left({n}\right)\left({W}\left({i}\right)\right)=\left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)\left({W}\left({i}\right)\right)$
595 516 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\subseteq ℝ$
596 465 ad2antlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {D}\left({n}\right):ℝ\underset{cn}{⟶}ℝ$
597 rescncf ${⊢}\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\subseteq ℝ\to \left({D}\left({n}\right):ℝ\underset{cn}{⟶}ℝ\to \left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right):\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\underset{cn}{⟶}ℝ\right)$
598 595 596 597 sylc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right):\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\underset{cn}{⟶}ℝ$
599 511 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}\right)\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]$
600 598 599 cnlimci ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)\left({W}\left({i}\right)\right)\in \left(\left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right){lim}_{ℂ}{W}\left({i}\right)\right)$
601 594 600 eqeltrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {D}\left({n}\right)\left({W}\left({i}\right)\right)\in \left(\left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right){lim}_{ℂ}{W}\left({i}\right)\right)$
602 524 a1i ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\subseteq \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]$
603 602 resabs1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {\left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}={{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}$
604 603 eqcomd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}={\left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}$
605 604 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}\right)=\left({\left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}\right)$
606 605 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}\right)=\left({\left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}\right)$
607 390 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}\right)\in ℝ$
608 404 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}+1\right)\in ℝ$
609 294 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}\right)<{W}\left({i}+1\right)$
610 471 ad2antlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {D}\left({n}\right):ℝ⟶ℂ$
611 610 595 fssresd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right):\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟶ℂ$
612 607 608 609 611 limciccioolb ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({\left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}\right)=\left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right){lim}_{ℂ}{W}\left({i}\right)$
613 606 612 eqtr2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right){lim}_{ℂ}{W}\left({i}\right)=\left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}\right)$
614 601 613 eleqtrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {D}\left({n}\right)\left({W}\left({i}\right)\right)\in \left(\left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}\right)\right)$
615 483 488 489 590 614 mullimcf ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {R}{D}\left({n}\right)\left({W}\left({i}\right)\right)\in \left(\left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)\left({s}\right)\left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right)\left({s}\right)\right){lim}_{ℂ}{W}\left({i}\right)\right)$
616 eqidd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)=\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)$
617 192 adantl ${⊢}\left(\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\wedge {x}={s}\right)\to {F}\left({X}+{x}\right)={F}\left({X}+{s}\right)$
618 simpr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)$
619 49 adantr ${⊢}\left({\phi }\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {F}:ℝ⟶ℂ$
620 619 383 ffvelrnd ${⊢}\left({\phi }\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {F}\left({X}+{s}\right)\in ℂ$
621 620 adantlr ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {F}\left({X}+{s}\right)\in ℂ$
622 616 617 618 621 fvmptd ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)\left({s}\right)={F}\left({X}+{s}\right)$
623 622 adantllr ${⊢}\left(\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)\left({s}\right)={F}\left({X}+{s}\right)$
624 fvres ${⊢}{s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\to \left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right)\left({s}\right)={D}\left({n}\right)\left({s}\right)$
625 624 adantl ${⊢}\left(\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to \left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right)\left({s}\right)={D}\left({n}\right)\left({s}\right)$
626 623 625 oveq12d ${⊢}\left(\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)\left({s}\right)\left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right)\left({s}\right)={F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)$
627 626 eqcomd ${⊢}\left(\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\wedge {s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)=\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)\left({s}\right)\left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right)\left({s}\right)$
628 627 mpteq2dva ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\right)=\left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)\left({s}\right)\left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right)\left({s}\right)\right)$
629 375 628 eqtr2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)\left({s}\right)\left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right)\left({s}\right)\right)={{G}↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}$
630 629 oveq1d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)\left({s}\right)\left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right)\left({s}\right)\right){lim}_{ℂ}{W}\left({i}\right)=\left({{G}↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}\right)$
631 615 630 eleqtrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {R}{D}\left({n}\right)\left({W}\left({i}\right)\right)\in \left(\left({{G}↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}\right)\right)$
632 455 426 ltned ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{x}\ne {Q}\left({i}+1\right)$
633 eldifsn ${⊢}{X}+{x}\in \left(\mathrm{dom}\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\setminus \left\{{Q}\left({i}+1\right)\right\}\right)↔\left({X}+{x}\in \mathrm{dom}\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\wedge {X}+{x}\ne {Q}\left({i}+1\right)\right)$
634 497 632 633 sylanbrc ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\right)\to {X}+{x}\in \left(\mathrm{dom}\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\setminus \left\{{Q}\left({i}+1\right)\right\}\right)$
635 634 ralrimiva ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \forall {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}{X}+{x}\in \left(\mathrm{dom}\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\setminus \left\{{Q}\left({i}+1\right)\right\}\right)$
636 503 rnmptss ${⊢}\forall {x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)\phantom{\rule{.4em}{0ex}}{X}+{x}\in \left(\mathrm{dom}\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\setminus \left\{{Q}\left({i}+1\right)\right\}\right)\to \mathrm{ran}\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)\subseteq \mathrm{dom}\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\setminus \left\{{Q}\left({i}+1\right)\right\}$
637 635 636 syl ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \mathrm{ran}\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)\subseteq \mathrm{dom}\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\setminus \left\{{Q}\left({i}+1\right)\right\}$
638 404 leidd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}+1\right)\le {W}\left({i}+1\right)$
639 390 404 404 510 638 eliccd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}+1\right)\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]$
640 521 639 cnlimci ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)\left({W}\left({i}+1\right)\right)\in \left(\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right){lim}_{ℂ}{W}\left({i}+1\right)\right)$
641 oveq2 ${⊢}{x}={W}\left({i}+1\right)\to {X}+{x}={X}+{W}\left({i}+1\right)$
642 641 adantl ${⊢}\left(\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\wedge {x}={W}\left({i}+1\right)\right)\to {X}+{x}={X}+{W}\left({i}+1\right)$
643 277 404 readdcld ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {X}+{W}\left({i}+1\right)\in ℝ$
644 506 642 639 643 fvmptd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)\left({W}\left({i}+1\right)\right)={X}+{W}\left({i}+1\right)$
645 644 424 eqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)\left({W}\left({i}+1\right)\right)={Q}\left({i}+1\right)$
646 528 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right){lim}_{ℂ}{W}\left({i}+1\right)=\left({\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}+1\right)$
647 390 404 294 539 limcicciooub ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}+1\right)=\left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right){lim}_{ℂ}{W}\left({i}+1\right)$
648 646 647 eqtr2d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({x}\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]⟼{X}+{x}\right){lim}_{ℂ}{W}\left({i}+1\right)=\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right){lim}_{ℂ}{W}\left({i}+1\right)$
649 640 645 648 3eltr3d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {Q}\left({i}+1\right)\in \left(\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right){lim}_{ℂ}{W}\left({i}+1\right)\right)$
650 637 649 14 limccog ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {L}\in \left(\left(\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\circ \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)\right){lim}_{ℂ}{W}\left({i}+1\right)\right)$
651 587 oveq1d ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left(\left({{F}↾}_{\left({Q}\left({i}\right),{Q}\left({i}+1\right)\right)}\right)\circ \left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{X}+{x}\right)\right){lim}_{ℂ}{W}\left({i}+1\right)=\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right){lim}_{ℂ}{W}\left({i}+1\right)$
652 650 651 eleqtrd ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {L}\in \left(\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right){lim}_{ℂ}{W}\left({i}+1\right)\right)$
653 652 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {L}\in \left(\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right){lim}_{ℂ}{W}\left({i}+1\right)\right)$
654 639 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {W}\left({i}+1\right)\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]$
655 598 654 cnlimci ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)\left({W}\left({i}+1\right)\right)\in \left(\left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right){lim}_{ℂ}{W}\left({i}+1\right)\right)$
656 fvres ${⊢}{W}\left({i}+1\right)\in \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\to \left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)\left({W}\left({i}+1\right)\right)={D}\left({n}\right)\left({W}\left({i}+1\right)\right)$
657 654 656 syl ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)\left({W}\left({i}+1\right)\right)={D}\left({n}\right)\left({W}\left({i}+1\right)\right)$
658 607 608 609 611 limcicciooub ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({\left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}+1\right)=\left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right){lim}_{ℂ}{W}\left({i}+1\right)$
659 658 eqcomd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right){lim}_{ℂ}{W}\left({i}+1\right)=\left({\left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}+1\right)$
660 resabs1 ${⊢}\left({W}\left({i}\right),{W}\left({i}+1\right)\right)\subseteq \left[{W}\left({i}\right),{W}\left({i}+1\right)\right]\to {\left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}={{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}$
661 524 660 mp1i ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {\left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}={{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}$
662 661 oveq1d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({\left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}+1\right)=\left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}+1\right)$
663 659 662 eqtrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{D}\left({n}\right)↾}_{\left[{W}\left({i}\right),{W}\left({i}+1\right)\right]}\right){lim}_{ℂ}{W}\left({i}+1\right)=\left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}+1\right)$
664 655 657 663 3eltr3d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {D}\left({n}\right)\left({W}\left({i}+1\right)\right)\in \left(\left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}+1\right)\right)$
665 483 488 489 653 664 mullimcf ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {L}{D}\left({n}\right)\left({W}\left({i}+1\right)\right)\in \left(\left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)\left({s}\right)\left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right)\left({s}\right)\right){lim}_{ℂ}{W}\left({i}+1\right)\right)$
666 629 oveq1d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({s}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼\left({x}\in \left({W}\left({i}\right),{W}\left({i}+1\right)\right)⟼{F}\left({X}+{x}\right)\right)\left({s}\right)\left({{D}\left({n}\right)↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right)\left({s}\right)\right){lim}_{ℂ}{W}\left({i}+1\right)=\left({{G}↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}+1\right)$
667 665 666 eleqtrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {L}{D}\left({n}\right)\left({W}\left({i}+1\right)\right)\in \left(\left({{G}↾}_{\left({W}\left({i}\right),{W}\left({i}+1\right)\right)}\right){lim}_{ℂ}{W}\left({i}+1\right)\right)$
668 130 133 225 226 16 114 300 211 369 478 631 667 fourierdlem110 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{\left[\left(-\mathrm{\pi }\right)-{X}-\left(-{X}\right),\mathrm{\pi }-{X}-\left(-{X}\right)\right]}{G}\left({x}\right)d{x}={\int }_{\left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]}{G}\left({x}\right)d{x}$
669 668 eqcomd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{\left[-\mathrm{\pi }-{X},\mathrm{\pi }-{X}\right]}{G}\left({x}\right)d{x}={\int }_{\left[\left(-\mathrm{\pi }\right)-{X}-\left(-{X}\right),\mathrm{\pi }-{X}-\left(-{X}\right)\right]}{G}\left({x}\right)d{x}$
670 129 recnd ${⊢}{\phi }\to -\mathrm{\pi }-{X}\in ℂ$
671 670 154 subnegd ${⊢}{\phi }\to \left(-\mathrm{\pi }\right)-{X}-\left(-{X}\right)$