# Metamath Proof Explorer

## Theorem fourierdlem95

Description: Algebraic manipulation of integrals, used by other lemmas. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

### Proof

Step Hyp Ref Expression
1 fourierdlem95.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
2 fourierdlem95.xre ${⊢}{\phi }\to {X}\in ℝ$
3 fourierdlem95.p ${⊢}{P}=\left({m}\in ℕ⟼\left\{{p}\in \left({ℝ}^{\left(0\dots {m}\right)}\right)|\left(\left({p}\left(0\right)=-\mathrm{\pi }+{X}\wedge {p}\left({m}\right)=\mathrm{\pi }+{X}\right)\wedge \forall {i}\in \left(0..^{m}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right)\right\}\right)$
4 fourierdlem95.m ${⊢}{\phi }\to {M}\in ℕ$
5 fourierdlem95.v ${⊢}{\phi }\to {V}\in {P}\left({M}\right)$
6 fourierdlem95.x ${⊢}{\phi }\to {X}\in \mathrm{ran}{V}$
7 fourierdlem95.fcn ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
8 fourierdlem95.r ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {R}\in \left(\left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right){lim}_{ℂ}{V}\left({i}\right)\right)$
9 fourierdlem95.l ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to {L}\in \left(\left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right){lim}_{ℂ}{V}\left({i}+1\right)\right)$
10 fourierdlem95.h ${⊢}{H}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({s}=0,0,\frac{{F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)}{{s}}\right)\right)$
11 fourierdlem95.k ${⊢}{K}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼if\left({s}=0,1,\frac{{s}}{2\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)$
12 fourierdlem95.u ${⊢}{U}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{H}\left({s}\right){K}\left({s}\right)\right)$
13 fourierdlem95.s ${⊢}{S}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}\right)$
14 fourierdlem95.g ${⊢}{G}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{U}\left({s}\right){S}\left({s}\right)\right)$
15 fourierdlem95.i ${⊢}{I}=ℝ\mathrm{D}{F}$
16 fourierdlem95.ifn ${⊢}\left({\phi }\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{I}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)⟶ℝ$
17 fourierdlem95.b ${⊢}{\phi }\to {B}\in \left(\left({{I}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
18 fourierdlem95.c ${⊢}{\phi }\to {C}\in \left(\left({{I}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
19 fourierdlem95.y ${⊢}{\phi }\to {Y}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
20 fourierdlem95.w ${⊢}{\phi }\to {W}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
21 fourierdlem95.admvol ${⊢}{\phi }\to {A}\in \mathrm{dom}vol$
22 fourierdlem95.ass ${⊢}{\phi }\to {A}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \left\{0\right\}$
23 fourierlemenplusacver2eqitgdirker.e ${⊢}{E}=\left({n}\in ℕ⟼\frac{{\int }_{{A}}{G}\left({s}\right)d{s}}{\mathrm{\pi }}\right)$
24 fourierdlem95.d ${⊢}{D}=\left({n}\in ℕ⟼\left({s}\in ℝ⟼if\left({s}\mathrm{mod}2\mathrm{\pi }=0,\frac{2{n}+1}{2\mathrm{\pi }},\frac{\mathrm{sin}\left({n}+\left(\frac{1}{2}\right)\right){s}}{2\mathrm{\pi }\mathrm{sin}\left(\frac{{s}}{2}\right)}\right)\right)\right)$
25 fourierdlem95.o ${⊢}{\phi }\to {O}\in ℝ$
26 fourierdlem95.ifeqo ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to if\left(0<{s},{Y},{W}\right)={O}$
27 fourierdlem95.itgdirker ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{{A}}{D}\left({n}\right)\left({s}\right)d{s}=\frac{1}{2}$
28 simpr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}\in ℕ$
29 22 difss2d ${⊢}{\phi }\to {A}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
30 29 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {A}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
31 30 sselda ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]$
32 1 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {F}:ℝ⟶ℝ$
33 2 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {X}\in ℝ$
34 ioossre ${⊢}\left({X},\mathrm{+\infty }\right)\subseteq ℝ$
35 34 a1i ${⊢}{\phi }\to \left({X},\mathrm{+\infty }\right)\subseteq ℝ$
36 1 35 fssresd ${⊢}{\phi }\to \left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right):\left({X},\mathrm{+\infty }\right)⟶ℝ$
37 ioosscn ${⊢}\left({X},\mathrm{+\infty }\right)\subseteq ℂ$
38 37 a1i ${⊢}{\phi }\to \left({X},\mathrm{+\infty }\right)\subseteq ℂ$
39 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
40 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
41 40 a1i ${⊢}{\phi }\to \mathrm{+\infty }\in {ℝ}^{*}$
42 2 ltpnfd ${⊢}{\phi }\to {X}<\mathrm{+\infty }$
43 39 41 2 42 lptioo1cn ${⊢}{\phi }\to {X}\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(\left({X},\mathrm{+\infty }\right)\right)$
44 36 38 43 19 limcrecl ${⊢}{\phi }\to {Y}\in ℝ$
45 44 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {Y}\in ℝ$
46 ioossre ${⊢}\left(\mathrm{-\infty },{X}\right)\subseteq ℝ$
47 46 a1i ${⊢}{\phi }\to \left(\mathrm{-\infty },{X}\right)\subseteq ℝ$
48 1 47 fssresd ${⊢}{\phi }\to \left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right):\left(\mathrm{-\infty },{X}\right)⟶ℝ$
49 ioosscn ${⊢}\left(\mathrm{-\infty },{X}\right)\subseteq ℂ$
50 49 a1i ${⊢}{\phi }\to \left(\mathrm{-\infty },{X}\right)\subseteq ℂ$
51 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
52 51 a1i ${⊢}{\phi }\to \mathrm{-\infty }\in {ℝ}^{*}$
53 2 mnfltd ${⊢}{\phi }\to \mathrm{-\infty }<{X}$
54 39 52 2 53 lptioo2cn ${⊢}{\phi }\to {X}\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(\left(\mathrm{-\infty },{X}\right)\right)$
55 48 50 54 20 limcrecl ${⊢}{\phi }\to {W}\in ℝ$
56 55 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {W}\in ℝ$
57 28 nnred ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {n}\in ℝ$
58 32 33 45 56 10 11 12 57 13 14 fourierdlem67 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {G}:\left[-\mathrm{\pi },\mathrm{\pi }\right]⟶ℝ$
59 58 ffvelrnda ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {G}\left({s}\right)\in ℝ$
60 31 59 syldan ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to {G}\left({s}\right)\in ℝ$
61 21 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {A}\in \mathrm{dom}vol$
62 58 feqmptd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {G}=\left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{G}\left({s}\right)\right)$
63 6 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {X}\in \mathrm{ran}{V}$
64 19 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {Y}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
65 20 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {W}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
66 4 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {M}\in ℕ$
67 5 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {V}\in {P}\left({M}\right)$
68 7 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)\underset{cn}{⟶}ℂ$
69 8 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {R}\in \left(\left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right){lim}_{ℂ}{V}\left({i}\right)\right)$
70 9 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to {L}\in \left(\left({{F}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right){lim}_{ℂ}{V}\left({i}+1\right)\right)$
71 fveq2 ${⊢}{j}={i}\to {V}\left({j}\right)={V}\left({i}\right)$
72 71 oveq1d ${⊢}{j}={i}\to {V}\left({j}\right)-{X}={V}\left({i}\right)-{X}$
73 72 cbvmptv ${⊢}\left({j}\in \left(0\dots {M}\right)⟼{V}\left({j}\right)-{X}\right)=\left({i}\in \left(0\dots {M}\right)⟼{V}\left({i}\right)-{X}\right)$
74 eqid ${⊢}\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)=\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)$
75 16 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {i}\in \left(0..^{M}\right)\right)\to \left({{I}↾}_{\left({V}\left({i}\right),{V}\left({i}+1\right)\right)}\right):\left({V}\left({i}\right),{V}\left({i}+1\right)\right)⟶ℝ$
76 17 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {B}\in \left(\left({{I}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
77 18 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {C}\in \left(\left({{I}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
78 3 32 63 64 65 10 11 12 57 13 14 66 67 68 69 70 73 74 15 75 76 77 fourierdlem88 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {G}\in {𝐿}^{1}$
79 62 78 eqeltrrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{G}\left({s}\right)\right)\in {𝐿}^{1}$
80 30 61 59 79 iblss ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({s}\in {A}⟼{G}\left({s}\right)\right)\in {𝐿}^{1}$
81 60 80 itgrecl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{{A}}{G}\left({s}\right)d{s}\in ℝ$
82 pire ${⊢}\mathrm{\pi }\in ℝ$
83 82 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \mathrm{\pi }\in ℝ$
84 pipos ${⊢}0<\mathrm{\pi }$
85 82 84 gt0ne0ii ${⊢}\mathrm{\pi }\ne 0$
86 85 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \mathrm{\pi }\ne 0$
87 81 83 86 redivcld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{{\int }_{{A}}{G}\left({s}\right)d{s}}{\mathrm{\pi }}\in ℝ$
88 23 fvmpt2 ${⊢}\left({n}\in ℕ\wedge \frac{{\int }_{{A}}{G}\left({s}\right)d{s}}{\mathrm{\pi }}\in ℝ\right)\to {E}\left({n}\right)=\frac{{\int }_{{A}}{G}\left({s}\right)d{s}}{\mathrm{\pi }}$
89 28 87 88 syl2anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {E}\left({n}\right)=\frac{{\int }_{{A}}{G}\left({s}\right)d{s}}{\mathrm{\pi }}$
90 25 recnd ${⊢}{\phi }\to {O}\in ℂ$
91 2cnd ${⊢}{\phi }\to 2\in ℂ$
92 2ne0 ${⊢}2\ne 0$
93 92 a1i ${⊢}{\phi }\to 2\ne 0$
94 90 91 93 divrecd ${⊢}{\phi }\to \frac{{O}}{2}={O}\left(\frac{1}{2}\right)$
95 94 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{{O}}{2}={O}\left(\frac{1}{2}\right)$
96 27 eqcomd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{1}{2}={\int }_{{A}}{D}\left({n}\right)\left({s}\right)d{s}$
97 96 oveq2d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {O}\left(\frac{1}{2}\right)={O}{\int }_{{A}}{D}\left({n}\right)\left({s}\right)d{s}$
98 95 97 eqtrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{{O}}{2}={O}{\int }_{{A}}{D}\left({n}\right)\left({s}\right)d{s}$
99 89 98 oveq12d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {E}\left({n}\right)+\left(\frac{{O}}{2}\right)=\left(\frac{{\int }_{{A}}{G}\left({s}\right)d{s}}{\mathrm{\pi }}\right)+{O}{\int }_{{A}}{D}\left({n}\right)\left({s}\right)d{s}$
100 22 sselda ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {s}\in \left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \left\{0\right\}\right)$
101 100 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to {s}\in \left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \left\{0\right\}\right)$
102 eqid ${⊢}\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \left\{0\right\}=\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \left\{0\right\}$
103 1 2 44 55 24 10 11 12 13 14 102 fourierdlem66 ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \left\{0\right\}\right)\right)\to {G}\left({s}\right)=\mathrm{\pi }\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)$
104 101 103 syldan ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to {G}\left({s}\right)=\mathrm{\pi }\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)$
105 104 itgeq2dv ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{{A}}{G}\left({s}\right)d{s}={\int }_{{A}}\mathrm{\pi }\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)d{s}$
106 105 oveq1d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{{\int }_{{A}}{G}\left({s}\right)d{s}}{\mathrm{\pi }}=\frac{{\int }_{{A}}\mathrm{\pi }\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)d{s}}{\mathrm{\pi }}$
107 83 recnd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \mathrm{\pi }\in ℂ$
108 1 adantr ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {F}:ℝ⟶ℝ$
109 2 adantr ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {X}\in ℝ$
110 difss ${⊢}\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \left\{0\right\}\subseteq \left[-\mathrm{\pi },\mathrm{\pi }\right]$
111 82 renegcli ${⊢}-\mathrm{\pi }\in ℝ$
112 iccssre ${⊢}\left(-\mathrm{\pi }\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \left[-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℝ$
113 111 82 112 mp2an ${⊢}\left[-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℝ$
114 110 113 sstri ${⊢}\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \left\{0\right\}\subseteq ℝ$
115 114 100 sseldi ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {s}\in ℝ$
116 109 115 readdcld ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {X}+{s}\in ℝ$
117 108 116 ffvelrnd ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {F}\left({X}+{s}\right)\in ℝ$
118 44 55 ifcld ${⊢}{\phi }\to if\left(0<{s},{Y},{W}\right)\in ℝ$
119 118 adantr ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to if\left(0<{s},{Y},{W}\right)\in ℝ$
120 117 119 resubcld ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\in ℝ$
121 120 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to {F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\in ℝ$
122 28 adantr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to {n}\in ℕ$
123 115 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to {s}\in ℝ$
124 24 dirkerre ${⊢}\left({n}\in ℕ\wedge {s}\in ℝ\right)\to {D}\left({n}\right)\left({s}\right)\in ℝ$
125 122 123 124 syl2anc ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to {D}\left({n}\right)\left({s}\right)\in ℝ$
126 121 125 remulcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to \left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)\in ℝ$
127 104 eqcomd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to \mathrm{\pi }\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)={G}\left({s}\right)$
128 127 oveq1d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to \frac{\mathrm{\pi }\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)}{\mathrm{\pi }}=\frac{{G}\left({s}\right)}{\mathrm{\pi }}$
129 picn ${⊢}\mathrm{\pi }\in ℂ$
130 129 a1i ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to \mathrm{\pi }\in ℂ$
131 126 recnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to \left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)\in ℂ$
132 85 a1i ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to \mathrm{\pi }\ne 0$
133 130 131 130 132 div23d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to \frac{\mathrm{\pi }\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)}{\mathrm{\pi }}=\left(\frac{\mathrm{\pi }}{\mathrm{\pi }}\right)\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)$
134 60 recnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to {G}\left({s}\right)\in ℂ$
135 134 130 132 divrec2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to \frac{{G}\left({s}\right)}{\mathrm{\pi }}=\left(\frac{1}{\mathrm{\pi }}\right){G}\left({s}\right)$
136 128 133 135 3eqtr3rd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to \left(\frac{1}{\mathrm{\pi }}\right){G}\left({s}\right)=\left(\frac{\mathrm{\pi }}{\mathrm{\pi }}\right)\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)$
137 129 85 dividi ${⊢}\frac{\mathrm{\pi }}{\mathrm{\pi }}=1$
138 137 a1i ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to \frac{\mathrm{\pi }}{\mathrm{\pi }}=1$
139 138 oveq1d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to \left(\frac{\mathrm{\pi }}{\mathrm{\pi }}\right)\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)=1\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)$
140 131 mulid2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to 1\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)=\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)$
141 136 139 140 3eqtrrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to \left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)=\left(\frac{1}{\mathrm{\pi }}\right){G}\left({s}\right)$
142 141 mpteq2dva ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({s}\in {A}⟼\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)\right)=\left({s}\in {A}⟼\left(\frac{1}{\mathrm{\pi }}\right){G}\left({s}\right)\right)$
143 107 86 reccld ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{1}{\mathrm{\pi }}\in ℂ$
144 143 60 80 iblmulc2 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({s}\in {A}⟼\left(\frac{1}{\mathrm{\pi }}\right){G}\left({s}\right)\right)\in {𝐿}^{1}$
145 142 144 eqeltrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({s}\in {A}⟼\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)\right)\in {𝐿}^{1}$
146 107 126 145 itgmulc2 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \mathrm{\pi }{\int }_{{A}}\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)d{s}={\int }_{{A}}\mathrm{\pi }\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)d{s}$
147 146 eqcomd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{{A}}\mathrm{\pi }\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)d{s}=\mathrm{\pi }{\int }_{{A}}\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)d{s}$
148 147 oveq1d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{{\int }_{{A}}\mathrm{\pi }\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)d{s}}{\mathrm{\pi }}=\frac{\mathrm{\pi }{\int }_{{A}}\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)d{s}}{\mathrm{\pi }}$
149 126 145 itgcl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{{A}}\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)d{s}\in ℂ$
150 149 107 86 divcan3d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{\mathrm{\pi }{\int }_{{A}}\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)d{s}}{\mathrm{\pi }}={\int }_{{A}}\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)d{s}$
151 106 148 150 3eqtrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \frac{{\int }_{{A}}{G}\left({s}\right)d{s}}{\mathrm{\pi }}={\int }_{{A}}\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)d{s}$
152 90 adantr ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {O}\in ℂ$
153 113 sseli ${⊢}{s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\to {s}\in ℝ$
154 153 124 sylan2 ${⊢}\left({n}\in ℕ\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {D}\left({n}\right)\left({s}\right)\in ℝ$
155 154 adantll ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]\right)\to {D}\left({n}\right)\left({s}\right)\in ℝ$
156 111 a1i ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to -\mathrm{\pi }\in ℝ$
157 ax-resscn ${⊢}ℝ\subseteq ℂ$
158 157 a1i ${⊢}{n}\in ℕ\to ℝ\subseteq ℂ$
159 ssid ${⊢}ℂ\subseteq ℂ$
160 cncfss
161 158 159 160 sylancl
162 eqid ${⊢}\left({s}\in ℝ⟼{D}\left({n}\right)\left({s}\right)\right)=\left({s}\in ℝ⟼{D}\left({n}\right)\left({s}\right)\right)$
163 24 dirkerf ${⊢}{n}\in ℕ\to {D}\left({n}\right):ℝ⟶ℝ$
164 163 feqmptd ${⊢}{n}\in ℕ\to {D}\left({n}\right)=\left({s}\in ℝ⟼{D}\left({n}\right)\left({s}\right)\right)$
165 24 dirkercncf ${⊢}{n}\in ℕ\to {D}\left({n}\right):ℝ\underset{cn}{⟶}ℝ$
166 164 165 eqeltrrd ${⊢}{n}\in ℕ\to \left({s}\in ℝ⟼{D}\left({n}\right)\left({s}\right)\right):ℝ\underset{cn}{⟶}ℝ$
167 113 a1i ${⊢}{n}\in ℕ\to \left[-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℝ$
168 ssid ${⊢}ℝ\subseteq ℝ$
169 168 a1i ${⊢}{n}\in ℕ\to ℝ\subseteq ℝ$
170 162 166 167 169 154 cncfmptssg ${⊢}{n}\in ℕ\to \left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{D}\left({n}\right)\left({s}\right)\right):\left[-\mathrm{\pi },\mathrm{\pi }\right]\underset{cn}{⟶}ℝ$
171 161 170 sseldd ${⊢}{n}\in ℕ\to \left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{D}\left({n}\right)\left({s}\right)\right):\left[-\mathrm{\pi },\mathrm{\pi }\right]\underset{cn}{⟶}ℂ$
172 171 adantl ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{D}\left({n}\right)\left({s}\right)\right):\left[-\mathrm{\pi },\mathrm{\pi }\right]\underset{cn}{⟶}ℂ$
173 cniccibl ${⊢}\left(-\mathrm{\pi }\in ℝ\wedge \mathrm{\pi }\in ℝ\wedge \left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{D}\left({n}\right)\left({s}\right)\right):\left[-\mathrm{\pi },\mathrm{\pi }\right]\underset{cn}{⟶}ℂ\right)\to \left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{D}\left({n}\right)\left({s}\right)\right)\in {𝐿}^{1}$
174 156 83 172 173 syl3anc ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({s}\in \left[-\mathrm{\pi },\mathrm{\pi }\right]⟼{D}\left({n}\right)\left({s}\right)\right)\in {𝐿}^{1}$
175 30 61 155 174 iblss ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({s}\in {A}⟼{D}\left({n}\right)\left({s}\right)\right)\in {𝐿}^{1}$
176 152 125 175 itgmulc2 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {O}{\int }_{{A}}{D}\left({n}\right)\left({s}\right)d{s}={\int }_{{A}}{O}{D}\left({n}\right)\left({s}\right)d{s}$
177 151 176 oveq12d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left(\frac{{\int }_{{A}}{G}\left({s}\right)d{s}}{\mathrm{\pi }}\right)+{O}{\int }_{{A}}{D}\left({n}\right)\left({s}\right)d{s}={\int }_{{A}}\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)d{s}+{\int }_{{A}}{O}{D}\left({n}\right)\left({s}\right)d{s}$
178 25 ad2antrr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to {O}\in ℝ$
179 178 125 remulcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to {O}{D}\left({n}\right)\left({s}\right)\in ℝ$
180 152 125 175 iblmulc2 ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to \left({s}\in {A}⟼{O}{D}\left({n}\right)\left({s}\right)\right)\in {𝐿}^{1}$
181 126 145 179 180 itgadd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{{A}}\left(\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)+{O}{D}\left({n}\right)\left({s}\right)\right)d{s}={\int }_{{A}}\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)d{s}+{\int }_{{A}}{O}{D}\left({n}\right)\left({s}\right)d{s}$
182 26 eqcomd ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {O}=if\left(0<{s},{Y},{W}\right)$
183 182 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to {O}=if\left(0<{s},{Y},{W}\right)$
184 183 oveq1d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to {O}{D}\left({n}\right)\left({s}\right)=if\left(0<{s},{Y},{W}\right){D}\left({n}\right)\left({s}\right)$
185 184 oveq2d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to \left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)+{O}{D}\left({n}\right)\left({s}\right)=\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)+if\left(0<{s},{Y},{W}\right){D}\left({n}\right)\left({s}\right)$
186 117 recnd ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to {F}\left({X}+{s}\right)\in ℂ$
187 186 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to {F}\left({X}+{s}\right)\in ℂ$
188 119 recnd ${⊢}\left({\phi }\wedge {s}\in {A}\right)\to if\left(0<{s},{Y},{W}\right)\in ℂ$
189 188 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to if\left(0<{s},{Y},{W}\right)\in ℂ$
190 125 recnd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to {D}\left({n}\right)\left({s}\right)\in ℂ$
191 187 189 190 subdird ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to \left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)={F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)-if\left(0<{s},{Y},{W}\right){D}\left({n}\right)\left({s}\right)$
192 191 oveq1d ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to \left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)+if\left(0<{s},{Y},{W}\right){D}\left({n}\right)\left({s}\right)={F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)-if\left(0<{s},{Y},{W}\right){D}\left({n}\right)\left({s}\right)+if\left(0<{s},{Y},{W}\right){D}\left({n}\right)\left({s}\right)$
193 187 190 mulcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to {F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)\in ℂ$
194 189 190 mulcld ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to if\left(0<{s},{Y},{W}\right){D}\left({n}\right)\left({s}\right)\in ℂ$
195 193 194 npcand ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to {F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)-if\left(0<{s},{Y},{W}\right){D}\left({n}\right)\left({s}\right)+if\left(0<{s},{Y},{W}\right){D}\left({n}\right)\left({s}\right)={F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)$
196 185 192 195 3eqtrd ${⊢}\left(\left({\phi }\wedge {n}\in ℕ\right)\wedge {s}\in {A}\right)\to \left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)+{O}{D}\left({n}\right)\left({s}\right)={F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)$
197 196 itgeq2dv ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{{A}}\left(\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)+{O}{D}\left({n}\right)\left({s}\right)\right)d{s}={\int }_{{A}}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}$
198 181 197 eqtr3d ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {\int }_{{A}}\left({F}\left({X}+{s}\right)-if\left(0<{s},{Y},{W}\right)\right){D}\left({n}\right)\left({s}\right)d{s}+{\int }_{{A}}{O}{D}\left({n}\right)\left({s}\right)d{s}={\int }_{{A}}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}$
199 99 177 198 3eqtrd ${⊢}\left({\phi }\wedge {n}\in ℕ\right)\to {E}\left({n}\right)+\left(\frac{{O}}{2}\right)={\int }_{{A}}{F}\left({X}+{s}\right){D}\left({n}\right)\left({s}\right)d{s}$