# Metamath Proof Explorer

## Theorem fourier2

Description: Fourier series convergence, for a piecewise smooth function. Here it is also proven the existence of the left and right limits of F at any given point X . See fourierd for a comparison. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourier2.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
fourier2.t ${⊢}{T}=2\mathrm{\pi }$
fourier2.per ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)$
fourier2.g ${⊢}{G}={{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}$
fourier2.dmdv ${⊢}{\phi }\to \left(-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}{G}\in \mathrm{Fin}$
fourier2.dvcn ${⊢}{\phi }\to {G}:\mathrm{dom}{G}\underset{cn}{⟶}ℂ$
fourier2.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$
fourier2.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$
fourier2.x ${⊢}{\phi }\to {X}\in ℝ$
fourier2.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)$
fourier2.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)$
Assertion fourier2 ${⊢}{\phi }\to \exists {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\phantom{\rule{.4em}{0ex}}\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}$

### Proof

Step Hyp Ref Expression
1 fourier2.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
2 fourier2.t ${⊢}{T}=2\mathrm{\pi }$
3 fourier2.per ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)$
4 fourier2.g ${⊢}{G}={{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}$
5 fourier2.dmdv ${⊢}{\phi }\to \left(-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}{G}\in \mathrm{Fin}$
6 fourier2.dvcn ${⊢}{\phi }\to {G}:\mathrm{dom}{G}\underset{cn}{⟶}ℂ$
7 fourier2.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 fourier2.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 fourier2.x ${⊢}{\phi }\to {X}\in ℝ$
10 fourier2.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)$
11 fourier2.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)$
12 1 2 3 4 5 6 7 8 9 fourierdlem106 ${⊢}{\phi }\to \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\ne \varnothing \wedge \left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\ne \varnothing \right)$
13 12 simpld ${⊢}{\phi }\to \left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\ne \varnothing$
14 n0 ${⊢}\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\ne \varnothing ↔\exists {l}\phantom{\rule{.4em}{0ex}}{l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
15 13 14 sylib ${⊢}{\phi }\to \exists {l}\phantom{\rule{.4em}{0ex}}{l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
16 simpr ${⊢}\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\to {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
17 12 simprd ${⊢}{\phi }\to \left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\ne \varnothing$
18 n0 ${⊢}\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\ne \varnothing ↔\exists {r}\phantom{\rule{.4em}{0ex}}{r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
19 17 18 sylib ${⊢}{\phi }\to \exists {r}\phantom{\rule{.4em}{0ex}}{r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
20 19 adantr ${⊢}\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\to \exists {r}\phantom{\rule{.4em}{0ex}}{r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
21 simpr ${⊢}\left(\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\wedge {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\right)\to {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
22 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\wedge {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\right)\to {F}:ℝ⟶ℝ$
23 3 ad4ant14 ${⊢}\left(\left(\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\wedge {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\right)\wedge {x}\in ℝ\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)$
24 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\wedge {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\right)\to \left(-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}{G}\in \mathrm{Fin}$
25 6 ad2antrr ${⊢}\left(\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\wedge {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\right)\to {G}:\mathrm{dom}{G}\underset{cn}{⟶}ℂ$
26 7 ad4ant14 ${⊢}\left(\left(\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\wedge {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\right)\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$
27 8 ad4ant14 ${⊢}\left(\left(\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\wedge {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\right)\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$
28 9 ad2antrr ${⊢}\left(\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\wedge {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\right)\to {X}\in ℝ$
29 16 adantr ${⊢}\left(\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\wedge {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\right)\to {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
30 22 2 23 4 24 25 26 27 28 29 21 10 11 fourierd ${⊢}\left(\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\wedge {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\right)\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}$
31 21 30 jca ${⊢}\left(\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\wedge {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\right)\to \left({r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\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)$
32 31 ex ${⊢}\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\to \left({r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\to \left({r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\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)\right)$
33 32 eximdv ${⊢}\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\to \left(\exists {r}\phantom{\rule{.4em}{0ex}}{r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\to \exists {r}\phantom{\rule{.4em}{0ex}}\left({r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\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)\right)$
34 20 33 mpd ${⊢}\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\to \exists {r}\phantom{\rule{.4em}{0ex}}\left({r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\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)$
35 df-rex ${⊢}\exists {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\phantom{\rule{.4em}{0ex}}\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}↔\exists {r}\phantom{\rule{.4em}{0ex}}\left({r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\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)$
36 34 35 sylibr ${⊢}\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\to \exists {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\phantom{\rule{.4em}{0ex}}\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}$
37 16 36 jca ${⊢}\left({\phi }\wedge {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\right)\to \left({l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\wedge \exists {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\phantom{\rule{.4em}{0ex}}\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)$
38 37 ex ${⊢}{\phi }\to \left({l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\to \left({l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\wedge \exists {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\phantom{\rule{.4em}{0ex}}\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)\right)$
39 38 eximdv ${⊢}{\phi }\to \left(\exists {l}\phantom{\rule{.4em}{0ex}}{l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\to \exists {l}\phantom{\rule{.4em}{0ex}}\left({l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\wedge \exists {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\phantom{\rule{.4em}{0ex}}\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)\right)$
40 15 39 mpd ${⊢}{\phi }\to \exists {l}\phantom{\rule{.4em}{0ex}}\left({l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\wedge \exists {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\phantom{\rule{.4em}{0ex}}\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)$
41 df-rex ${⊢}\exists {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\phantom{\rule{.4em}{0ex}}\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}↔\exists {l}\phantom{\rule{.4em}{0ex}}\left({l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\wedge \exists {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\phantom{\rule{.4em}{0ex}}\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)$
42 40 41 sylibr ${⊢}{\phi }\to \exists {l}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)\phantom{\rule{.4em}{0ex}}\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}$