# Metamath Proof Explorer

## Theorem fourierdlem115

Description: Fourier serier convergence, for piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem115.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
fourierdlem115.t ${⊢}{T}=2\mathrm{\pi }$
fourierdlem115.per ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)$
fourierdlem115.g ${⊢}{G}={{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}$
fourierdlem115.dmdv ${⊢}{\phi }\to \left(-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}{G}\in \mathrm{Fin}$
fourierdlem115.dvcn ${⊢}{\phi }\to {G}:\mathrm{dom}{G}\underset{cn}{⟶}ℂ$
fourierdlem115.rlim ${⊢}\left({\phi }\wedge {x}\in \left(\left[-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}{G}\right)\right)\to \left({{G}↾}_{\left({x},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{x}\ne \varnothing$
fourierdlem115.llim ${⊢}\left({\phi }\wedge {x}\in \left(\left(-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}{G}\right)\right)\to \left({{G}↾}_{\left(\mathrm{-\infty },{x}\right)}\right){lim}_{ℂ}{x}\ne \varnothing$
fourierdlem115.x ${⊢}{\phi }\to {X}\in ℝ$
fourierdlem115.l ${⊢}{\phi }\to {L}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
fourierdlem115.r ${⊢}{\phi }\to {R}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
fourierdlem115.a ${⊢}{A}=\left({n}\in {ℕ}_{0}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{n}{x}d{x}}{\mathrm{\pi }}\right)$
fourierdlem115.b ${⊢}{B}=\left({n}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{n}{x}d{x}}{\mathrm{\pi }}\right)$
fourierdlem115.s ${⊢}{S}=\left({k}\in ℕ⟼{A}\left({k}\right)\mathrm{cos}{k}{X}+{B}\left({k}\right)\mathrm{sin}{k}{X}\right)$
Assertion fourierdlem115 ${⊢}{\phi }\to \left(seq1\left(+,{S}\right)⇝\left(\left(\frac{{L}+{R}}{2}\right)-\left(\frac{{A}\left(0\right)}{2}\right)\right)\wedge \left(\frac{{A}\left(0\right)}{2}\right)+\sum _{{n}\in ℕ}\left({A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)=\frac{{L}+{R}}{2}\right)$

### Proof

Step Hyp Ref Expression
1 fourierdlem115.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
2 fourierdlem115.t ${⊢}{T}=2\mathrm{\pi }$
3 fourierdlem115.per ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)$
4 fourierdlem115.g ${⊢}{G}={{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}$
5 fourierdlem115.dmdv ${⊢}{\phi }\to \left(-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}{G}\in \mathrm{Fin}$
6 fourierdlem115.dvcn ${⊢}{\phi }\to {G}:\mathrm{dom}{G}\underset{cn}{⟶}ℂ$
7 fourierdlem115.rlim ${⊢}\left({\phi }\wedge {x}\in \left(\left[-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}{G}\right)\right)\to \left({{G}↾}_{\left({x},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{x}\ne \varnothing$
8 fourierdlem115.llim ${⊢}\left({\phi }\wedge {x}\in \left(\left(-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}{G}\right)\right)\to \left({{G}↾}_{\left(\mathrm{-\infty },{x}\right)}\right){lim}_{ℂ}{x}\ne \varnothing$
9 fourierdlem115.x ${⊢}{\phi }\to {X}\in ℝ$
10 fourierdlem115.l ${⊢}{\phi }\to {L}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
11 fourierdlem115.r ${⊢}{\phi }\to {R}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
12 fourierdlem115.a ${⊢}{A}=\left({n}\in {ℕ}_{0}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{n}{x}d{x}}{\mathrm{\pi }}\right)$
13 fourierdlem115.b ${⊢}{B}=\left({n}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{n}{x}d{x}}{\mathrm{\pi }}\right)$
14 fourierdlem115.s ${⊢}{S}=\left({k}\in ℕ⟼{A}\left({k}\right)\mathrm{cos}{k}{X}+{B}\left({k}\right)\mathrm{sin}{k}{X}\right)$
15 oveq1 ${⊢}{n}={k}\to {n}{x}={k}{x}$
16 15 fveq2d ${⊢}{n}={k}\to \mathrm{cos}{n}{x}=\mathrm{cos}{k}{x}$
17 16 oveq2d ${⊢}{n}={k}\to {F}\left({x}\right)\mathrm{cos}{n}{x}={F}\left({x}\right)\mathrm{cos}{k}{x}$
18 17 adantr ${⊢}\left({n}={k}\wedge {x}\in \left(-\mathrm{\pi },\mathrm{\pi }\right)\right)\to {F}\left({x}\right)\mathrm{cos}{n}{x}={F}\left({x}\right)\mathrm{cos}{k}{x}$
19 18 itgeq2dv ${⊢}{n}={k}\to {\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{n}{x}d{x}={\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{k}{x}d{x}$
20 19 oveq1d ${⊢}{n}={k}\to \frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{n}{x}d{x}}{\mathrm{\pi }}=\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{k}{x}d{x}}{\mathrm{\pi }}$
21 20 cbvmptv ${⊢}\left({n}\in {ℕ}_{0}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{n}{x}d{x}}{\mathrm{\pi }}\right)=\left({k}\in {ℕ}_{0}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{k}{x}d{x}}{\mathrm{\pi }}\right)$
22 12 21 eqtri ${⊢}{A}=\left({k}\in {ℕ}_{0}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{k}{x}d{x}}{\mathrm{\pi }}\right)$
23 15 fveq2d ${⊢}{n}={k}\to \mathrm{sin}{n}{x}=\mathrm{sin}{k}{x}$
24 23 oveq2d ${⊢}{n}={k}\to {F}\left({x}\right)\mathrm{sin}{n}{x}={F}\left({x}\right)\mathrm{sin}{k}{x}$
25 24 adantr ${⊢}\left({n}={k}\wedge {x}\in \left(-\mathrm{\pi },\mathrm{\pi }\right)\right)\to {F}\left({x}\right)\mathrm{sin}{n}{x}={F}\left({x}\right)\mathrm{sin}{k}{x}$
26 25 itgeq2dv ${⊢}{n}={k}\to {\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{n}{x}d{x}={\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{k}{x}d{x}$
27 26 oveq1d ${⊢}{n}={k}\to \frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{n}{x}d{x}}{\mathrm{\pi }}=\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{k}{x}d{x}}{\mathrm{\pi }}$
28 27 cbvmptv ${⊢}\left({n}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{n}{x}d{x}}{\mathrm{\pi }}\right)=\left({k}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{k}{x}d{x}}{\mathrm{\pi }}\right)$
29 13 28 eqtri ${⊢}{B}=\left({k}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{k}{x}d{x}}{\mathrm{\pi }}\right)$
30 eqid ${⊢}\left({k}\in ℕ⟼\left\{{w}\in \left({ℝ}^{\left(0\dots {k}\right)}\right)|\left(\left({w}\left(0\right)=-\mathrm{\pi }\wedge {w}\left({k}\right)=\mathrm{\pi }\right)\wedge \forall {z}\in \left(0..^{k}\right)\phantom{\rule{.4em}{0ex}}{w}\left({z}\right)<{w}\left({z}+1\right)\right)\right\}\right)=\left({k}\in ℕ⟼\left\{{w}\in \left({ℝ}^{\left(0\dots {k}\right)}\right)|\left(\left({w}\left(0\right)=-\mathrm{\pi }\wedge {w}\left({k}\right)=\mathrm{\pi }\right)\wedge \forall {z}\in \left(0..^{k}\right)\phantom{\rule{.4em}{0ex}}{w}\left({z}\right)<{w}\left({z}+1\right)\right)\right\}\right)$
31 id ${⊢}{y}={x}\to {y}={x}$
32 oveq2 ${⊢}{y}={x}\to \mathrm{\pi }-{y}=\mathrm{\pi }-{x}$
33 32 oveq1d ${⊢}{y}={x}\to \frac{\mathrm{\pi }-{y}}{{T}}=\frac{\mathrm{\pi }-{x}}{{T}}$
34 33 fveq2d ${⊢}{y}={x}\to ⌊\frac{\mathrm{\pi }-{y}}{{T}}⌋=⌊\frac{\mathrm{\pi }-{x}}{{T}}⌋$
35 34 oveq1d ${⊢}{y}={x}\to ⌊\frac{\mathrm{\pi }-{y}}{{T}}⌋{T}=⌊\frac{\mathrm{\pi }-{x}}{{T}}⌋{T}$
36 31 35 oveq12d ${⊢}{y}={x}\to {y}+⌊\frac{\mathrm{\pi }-{y}}{{T}}⌋{T}={x}+⌊\frac{\mathrm{\pi }-{x}}{{T}}⌋{T}$
37 36 cbvmptv ${⊢}\left({y}\in ℝ⟼{y}+⌊\frac{\mathrm{\pi }-{y}}{{T}}⌋{T}\right)=\left({x}\in ℝ⟼{x}+⌊\frac{\mathrm{\pi }-{x}}{{T}}⌋{T}\right)$
38 eqid ${⊢}\left\{-\mathrm{\pi },\mathrm{\pi },\left({y}\in ℝ⟼{y}+⌊\frac{\mathrm{\pi }-{y}}{{T}}⌋{T}\right)\left({X}\right)\right\}\cup \left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}{G}\right)=\left\{-\mathrm{\pi },\mathrm{\pi },\left({y}\in ℝ⟼{y}+⌊\frac{\mathrm{\pi }-{y}}{{T}}⌋{T}\right)\left({X}\right)\right\}\cup \left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}{G}\right)$
39 eqid ${⊢}\left|\left\{-\mathrm{\pi },\mathrm{\pi },\left({y}\in ℝ⟼{y}+⌊\frac{\mathrm{\pi }-{y}}{{T}}⌋{T}\right)\left({X}\right)\right\}\cup \left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}{G}\right)\right|-1=\left|\left\{-\mathrm{\pi },\mathrm{\pi },\left({y}\in ℝ⟼{y}+⌊\frac{\mathrm{\pi }-{y}}{{T}}⌋{T}\right)\left({X}\right)\right\}\cup \left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}{G}\right)\right|-1$
40 isoeq1 ${⊢}{g}={f}\to \left({g}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi },\mathrm{\pi },\left({y}\in ℝ⟼{y}+⌊\frac{\mathrm{\pi }-{y}}{{T}}⌋{T}\right)\left({X}\right)\right\}\cup \left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}{G}\right)\right|-1\right),\left\{-\mathrm{\pi },\mathrm{\pi },\left({y}\in ℝ⟼{y}+⌊\frac{\mathrm{\pi }-{y}}{{T}}⌋{T}\right)\left({X}\right)\right\}\cup \left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}{G}\right)\right)↔{f}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi },\mathrm{\pi },\left({y}\in ℝ⟼{y}+⌊\frac{\mathrm{\pi }-{y}}{{T}}⌋{T}\right)\left({X}\right)\right\}\cup \left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}{G}\right)\right|-1\right),\left\{-\mathrm{\pi },\mathrm{\pi },\left({y}\in ℝ⟼{y}+⌊\frac{\mathrm{\pi }-{y}}{{T}}⌋{T}\right)\left({X}\right)\right\}\cup \left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}{G}\right)\right)\right)$
41 40 cbviotavw ${⊢}\left(\iota {g}|{g}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi },\mathrm{\pi },\left({y}\in ℝ⟼{y}+⌊\frac{\mathrm{\pi }-{y}}{{T}}⌋{T}\right)\left({X}\right)\right\}\cup \left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}{G}\right)\right|-1\right),\left\{-\mathrm{\pi },\mathrm{\pi },\left({y}\in ℝ⟼{y}+⌊\frac{\mathrm{\pi }-{y}}{{T}}⌋{T}\right)\left({X}\right)\right\}\cup \left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}{G}\right)\right)\right)=\left(\iota {f}|{f}{Isom}_{<,<}\left(\left(0\dots \left|\left\{-\mathrm{\pi },\mathrm{\pi },\left({y}\in ℝ⟼{y}+⌊\frac{\mathrm{\pi }-{y}}{{T}}⌋{T}\right)\left({X}\right)\right\}\cup \left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}{G}\right)\right|-1\right),\left\{-\mathrm{\pi },\mathrm{\pi },\left({y}\in ℝ⟼{y}+⌊\frac{\mathrm{\pi }-{y}}{{T}}⌋{T}\right)\left({X}\right)\right\}\cup \left(\left[-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}{G}\right)\right)\right)$
42 1 2 3 4 5 6 7 8 9 10 11 22 29 14 30 37 38 39 41 fourierdlem114 ${⊢}{\phi }\to \left(seq1\left(+,{S}\right)⇝\left(\left(\frac{{L}+{R}}{2}\right)-\left(\frac{{A}\left(0\right)}{2}\right)\right)\wedge \left(\frac{{A}\left(0\right)}{2}\right)+\sum _{{k}\in ℕ}\left({A}\left({k}\right)\mathrm{cos}{k}{X}+{B}\left({k}\right)\mathrm{sin}{k}{X}\right)=\frac{{L}+{R}}{2}\right)$
43 42 simpld ${⊢}{\phi }\to seq1\left(+,{S}\right)⇝\left(\left(\frac{{L}+{R}}{2}\right)-\left(\frac{{A}\left(0\right)}{2}\right)\right)$
44 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)$
45 nfmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in {ℕ}_{0}⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{cos}{n}{x}d{x}}{\mathrm{\pi }}\right)$
46 12 45 nfcxfr ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{A}$
47 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{k}$
48 46 47 nffv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{A}\left({k}\right)$
49 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}×$
50 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\mathrm{cos}{k}{X}$
51 48 49 50 nfov ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{A}\left({k}\right)\mathrm{cos}{k}{X}$
52 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}+$
53 nfmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in ℕ⟼\frac{{\int }_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}{F}\left({x}\right)\mathrm{sin}{n}{x}d{x}}{\mathrm{\pi }}\right)$
54 13 53 nfcxfr ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{B}$
55 54 47 nffv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{B}\left({k}\right)$
56 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\mathrm{sin}{k}{X}$
57 55 49 56 nfov ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{B}\left({k}\right)\mathrm{sin}{k}{X}$
58 51 52 57 nfov ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({A}\left({k}\right)\mathrm{cos}{k}{X}+{B}\left({k}\right)\mathrm{sin}{k}{X}\right)$
59 fveq2 ${⊢}{n}={k}\to {A}\left({n}\right)={A}\left({k}\right)$
60 oveq1 ${⊢}{n}={k}\to {n}{X}={k}{X}$
61 60 fveq2d ${⊢}{n}={k}\to \mathrm{cos}{n}{X}=\mathrm{cos}{k}{X}$
62 59 61 oveq12d ${⊢}{n}={k}\to {A}\left({n}\right)\mathrm{cos}{n}{X}={A}\left({k}\right)\mathrm{cos}{k}{X}$
63 fveq2 ${⊢}{n}={k}\to {B}\left({n}\right)={B}\left({k}\right)$
64 60 fveq2d ${⊢}{n}={k}\to \mathrm{sin}{n}{X}=\mathrm{sin}{k}{X}$
65 63 64 oveq12d ${⊢}{n}={k}\to {B}\left({n}\right)\mathrm{sin}{n}{X}={B}\left({k}\right)\mathrm{sin}{k}{X}$
66 62 65 oveq12d ${⊢}{n}={k}\to {A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}={A}\left({k}\right)\mathrm{cos}{k}{X}+{B}\left({k}\right)\mathrm{sin}{k}{X}$
67 44 58 66 cbvsumi ${⊢}\sum _{{n}\in ℕ}\left({A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)=\sum _{{k}\in ℕ}\left({A}\left({k}\right)\mathrm{cos}{k}{X}+{B}\left({k}\right)\mathrm{sin}{k}{X}\right)$
68 67 oveq2i ${⊢}\left(\frac{{A}\left(0\right)}{2}\right)+\sum _{{n}\in ℕ}\left({A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)=\left(\frac{{A}\left(0\right)}{2}\right)+\sum _{{k}\in ℕ}\left({A}\left({k}\right)\mathrm{cos}{k}{X}+{B}\left({k}\right)\mathrm{sin}{k}{X}\right)$
69 42 simprd ${⊢}{\phi }\to \left(\frac{{A}\left(0\right)}{2}\right)+\sum _{{k}\in ℕ}\left({A}\left({k}\right)\mathrm{cos}{k}{X}+{B}\left({k}\right)\mathrm{sin}{k}{X}\right)=\frac{{L}+{R}}{2}$
70 68 69 syl5eq ${⊢}{\phi }\to \left(\frac{{A}\left(0\right)}{2}\right)+\sum _{{n}\in ℕ}\left({A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)=\frac{{L}+{R}}{2}$
71 43 70 jca ${⊢}{\phi }\to \left(seq1\left(+,{S}\right)⇝\left(\left(\frac{{L}+{R}}{2}\right)-\left(\frac{{A}\left(0\right)}{2}\right)\right)\wedge \left(\frac{{A}\left(0\right)}{2}\right)+\sum _{{n}\in ℕ}\left({A}\left({n}\right)\mathrm{cos}{n}{X}+{B}\left({n}\right)\mathrm{sin}{n}{X}\right)=\frac{{L}+{R}}{2}\right)$