# Metamath Proof Explorer

## Theorem fouriercn

Description: If the derivative of F is continuous, then the Fourier series for F converges to F everywhere and the hypothesis are simpler than those for the more general case of a piecewise smooth function (see fourierd for a comparison). (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fouriercn.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
fouriercn.t ${⊢}{T}=2\mathrm{\pi }$
fouriercn.per ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)$
fouriercn.dv ${⊢}{\phi }\to {{F}}_{ℝ}^{\prime }:ℝ\underset{cn}{⟶}ℂ$
fouriercn.g ${⊢}{G}={{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}$
fouriercn.x ${⊢}{\phi }\to {X}\in ℝ$
fouriercn.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)$
fouriercn.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 fouriercn ${⊢}{\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)={F}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 fouriercn.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
2 fouriercn.t ${⊢}{T}=2\mathrm{\pi }$
3 fouriercn.per ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)$
4 fouriercn.dv ${⊢}{\phi }\to {{F}}_{ℝ}^{\prime }:ℝ\underset{cn}{⟶}ℂ$
5 fouriercn.g ${⊢}{G}={{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}$
6 fouriercn.x ${⊢}{\phi }\to {X}\in ℝ$
7 fouriercn.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)$
8 fouriercn.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)$
9 5 dmeqi ${⊢}\mathrm{dom}{G}=\mathrm{dom}\left({{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}\right)$
10 ioossre ${⊢}\left(-\mathrm{\pi },\mathrm{\pi }\right)\subseteq ℝ$
11 cncff ${⊢}{{F}}_{ℝ}^{\prime }:ℝ\underset{cn}{⟶}ℂ\to {{F}}_{ℝ}^{\prime }:ℝ⟶ℂ$
12 fdm ${⊢}{{F}}_{ℝ}^{\prime }:ℝ⟶ℂ\to \mathrm{dom}{{F}}_{ℝ}^{\prime }=ℝ$
13 4 11 12 3syl ${⊢}{\phi }\to \mathrm{dom}{{F}}_{ℝ}^{\prime }=ℝ$
14 10 13 sseqtrrid ${⊢}{\phi }\to \left(-\mathrm{\pi },\mathrm{\pi }\right)\subseteq \mathrm{dom}{{F}}_{ℝ}^{\prime }$
15 ssdmres ${⊢}\left(-\mathrm{\pi },\mathrm{\pi }\right)\subseteq \mathrm{dom}{{F}}_{ℝ}^{\prime }↔\mathrm{dom}\left({{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}\right)=\left(-\mathrm{\pi },\mathrm{\pi }\right)$
16 14 15 sylib ${⊢}{\phi }\to \mathrm{dom}\left({{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}\right)=\left(-\mathrm{\pi },\mathrm{\pi }\right)$
17 9 16 syl5eq ${⊢}{\phi }\to \mathrm{dom}{G}=\left(-\mathrm{\pi },\mathrm{\pi }\right)$
18 17 difeq2d ${⊢}{\phi }\to \left(-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}{G}=\left(-\mathrm{\pi },\mathrm{\pi }\right)\setminus \left(-\mathrm{\pi },\mathrm{\pi }\right)$
19 difid ${⊢}\left(-\mathrm{\pi },\mathrm{\pi }\right)\setminus \left(-\mathrm{\pi },\mathrm{\pi }\right)=\varnothing$
20 18 19 syl6eq ${⊢}{\phi }\to \left(-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}{G}=\varnothing$
21 0fin ${⊢}\varnothing \in \mathrm{Fin}$
22 20 21 eqeltrdi ${⊢}{\phi }\to \left(-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}{G}\in \mathrm{Fin}$
23 rescncf ${⊢}\left(-\mathrm{\pi },\mathrm{\pi }\right)\subseteq ℝ\to \left({{F}}_{ℝ}^{\prime }:ℝ\underset{cn}{⟶}ℂ\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}\right):\left(-\mathrm{\pi },\mathrm{\pi }\right)\underset{cn}{⟶}ℂ\right)$
24 10 4 23 mpsyl ${⊢}{\phi }\to \left({{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}\right):\left(-\mathrm{\pi },\mathrm{\pi }\right)\underset{cn}{⟶}ℂ$
25 5 a1i ${⊢}{\phi }\to {G}={{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}$
26 17 oveq1d
27 24 25 26 3eltr4d ${⊢}{\phi }\to {G}:\mathrm{dom}{G}\underset{cn}{⟶}ℂ$
28 pire ${⊢}\mathrm{\pi }\in ℝ$
29 28 renegcli ${⊢}-\mathrm{\pi }\in ℝ$
30 28 rexri ${⊢}\mathrm{\pi }\in {ℝ}^{*}$
31 icossre ${⊢}\left(-\mathrm{\pi }\in ℝ\wedge \mathrm{\pi }\in {ℝ}^{*}\right)\to \left[-\mathrm{\pi },\mathrm{\pi }\right)\subseteq ℝ$
32 29 30 31 mp2an ${⊢}\left[-\mathrm{\pi },\mathrm{\pi }\right)\subseteq ℝ$
33 eldifi ${⊢}{x}\in \left(\left[-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}{G}\right)\to {x}\in \left[-\mathrm{\pi },\mathrm{\pi }\right)$
34 32 33 sseldi ${⊢}{x}\in \left(\left[-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}{G}\right)\to {x}\in ℝ$
35 limcresi ${⊢}{{F}}_{ℝ}^{\prime }{lim}_{ℂ}{x}\subseteq \left({{{F}}_{ℝ}^{\prime }↾}_{\left(\left(-\mathrm{\pi },\mathrm{\pi }\right)\cap \left({x},\mathrm{+\infty }\right)\right)}\right){lim}_{ℂ}{x}$
36 5 reseq1i ${⊢}{{G}↾}_{\left({x},\mathrm{+\infty }\right)}={\left({{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}\right)↾}_{\left({x},\mathrm{+\infty }\right)}$
37 resres ${⊢}{\left({{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}\right)↾}_{\left({x},\mathrm{+\infty }\right)}={{{F}}_{ℝ}^{\prime }↾}_{\left(\left(-\mathrm{\pi },\mathrm{\pi }\right)\cap \left({x},\mathrm{+\infty }\right)\right)}$
38 36 37 eqtr2i ${⊢}{{{F}}_{ℝ}^{\prime }↾}_{\left(\left(-\mathrm{\pi },\mathrm{\pi }\right)\cap \left({x},\mathrm{+\infty }\right)\right)}={{G}↾}_{\left({x},\mathrm{+\infty }\right)}$
39 38 oveq1i ${⊢}\left({{{F}}_{ℝ}^{\prime }↾}_{\left(\left(-\mathrm{\pi },\mathrm{\pi }\right)\cap \left({x},\mathrm{+\infty }\right)\right)}\right){lim}_{ℂ}{x}=\left({{G}↾}_{\left({x},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{x}$
40 35 39 sseqtri ${⊢}{{F}}_{ℝ}^{\prime }{lim}_{ℂ}{x}\subseteq \left({{G}↾}_{\left({x},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{x}$
41 4 adantr ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {{F}}_{ℝ}^{\prime }:ℝ\underset{cn}{⟶}ℂ$
42 simpr ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {x}\in ℝ$
43 41 42 cnlimci ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {{F}}_{ℝ}^{\prime }\left({x}\right)\in \left({{F}}_{ℝ}^{\prime }{lim}_{ℂ}{x}\right)$
44 40 43 sseldi ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {{F}}_{ℝ}^{\prime }\left({x}\right)\in \left(\left({{G}↾}_{\left({x},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{x}\right)$
45 44 ne0d ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({{G}↾}_{\left({x},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{x}\ne \varnothing$
46 34 45 sylan2 ${⊢}\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$
47 negpitopissre ${⊢}\left(-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℝ$
48 eldifi ${⊢}{x}\in \left(\left(-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}{G}\right)\to {x}\in \left(-\mathrm{\pi },\mathrm{\pi }\right]$
49 47 48 sseldi ${⊢}{x}\in \left(\left(-\mathrm{\pi },\mathrm{\pi }\right]\setminus \mathrm{dom}{G}\right)\to {x}\in ℝ$
50 limcresi ${⊢}{{F}}_{ℝ}^{\prime }{lim}_{ℂ}{x}\subseteq \left({{{F}}_{ℝ}^{\prime }↾}_{\left(\left(-\mathrm{\pi },\mathrm{\pi }\right)\cap \left(\mathrm{-\infty },{x}\right)\right)}\right){lim}_{ℂ}{x}$
51 5 reseq1i ${⊢}{{G}↾}_{\left(\mathrm{-\infty },{x}\right)}={\left({{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}\right)↾}_{\left(\mathrm{-\infty },{x}\right)}$
52 resres ${⊢}{\left({{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}\right)↾}_{\left(\mathrm{-\infty },{x}\right)}={{{F}}_{ℝ}^{\prime }↾}_{\left(\left(-\mathrm{\pi },\mathrm{\pi }\right)\cap \left(\mathrm{-\infty },{x}\right)\right)}$
53 51 52 eqtr2i ${⊢}{{{F}}_{ℝ}^{\prime }↾}_{\left(\left(-\mathrm{\pi },\mathrm{\pi }\right)\cap \left(\mathrm{-\infty },{x}\right)\right)}={{G}↾}_{\left(\mathrm{-\infty },{x}\right)}$
54 53 oveq1i ${⊢}\left({{{F}}_{ℝ}^{\prime }↾}_{\left(\left(-\mathrm{\pi },\mathrm{\pi }\right)\cap \left(\mathrm{-\infty },{x}\right)\right)}\right){lim}_{ℂ}{x}=\left({{G}↾}_{\left(\mathrm{-\infty },{x}\right)}\right){lim}_{ℂ}{x}$
55 50 54 sseqtri ${⊢}{{F}}_{ℝ}^{\prime }{lim}_{ℂ}{x}\subseteq \left({{G}↾}_{\left(\mathrm{-\infty },{x}\right)}\right){lim}_{ℂ}{x}$
56 55 43 sseldi ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {{F}}_{ℝ}^{\prime }\left({x}\right)\in \left(\left({{G}↾}_{\left(\mathrm{-\infty },{x}\right)}\right){lim}_{ℂ}{x}\right)$
57 56 ne0d ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left({{G}↾}_{\left(\mathrm{-\infty },{x}\right)}\right){lim}_{ℂ}{x}\ne \varnothing$
58 49 57 sylan2 ${⊢}\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$
59 eqid ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
60 ax-resscn ${⊢}ℝ\subseteq ℂ$
61 60 a1i ${⊢}{\phi }\to ℝ\subseteq ℂ$
62 1 61 fssd ${⊢}{\phi }\to {F}:ℝ⟶ℂ$
63 ssid ${⊢}ℝ\subseteq ℝ$
64 63 a1i ${⊢}{\phi }\to ℝ\subseteq ℝ$
65 dvcn ${⊢}\left(\left(ℝ\subseteq ℂ\wedge {F}:ℝ⟶ℂ\wedge ℝ\subseteq ℝ\right)\wedge \mathrm{dom}{{F}}_{ℝ}^{\prime }=ℝ\right)\to {F}:ℝ\underset{cn}{⟶}ℂ$
66 61 62 64 13 65 syl31anc ${⊢}{\phi }\to {F}:ℝ\underset{cn}{⟶}ℂ$
67 cncffvrn ${⊢}\left(ℝ\subseteq ℂ\wedge {F}:ℝ\underset{cn}{⟶}ℂ\right)\to \left({F}:ℝ\underset{cn}{⟶}ℝ↔{F}:ℝ⟶ℝ\right)$
68 61 66 67 syl2anc ${⊢}{\phi }\to \left({F}:ℝ\underset{cn}{⟶}ℝ↔{F}:ℝ⟶ℝ\right)$
69 1 68 mpbird ${⊢}{\phi }\to {F}:ℝ\underset{cn}{⟶}ℝ$
70 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
71 70 tgioo2 ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
72 70 71 71 cncfcn
73 61 61 72 syl2anc
74 69 73 eleqtrd ${⊢}{\phi }\to {F}\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$
75 uniretop ${⊢}ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
76 75 cncnpi ${⊢}\left({F}\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{Cn}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\wedge {X}\in ℝ\right)\to {F}\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{CnP}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left({X}\right)$
77 74 6 76 syl2anc ${⊢}{\phi }\to {F}\in \left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\mathrm{CnP}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left({X}\right)$
78 1 2 3 5 22 27 46 58 59 77 7 8 fouriercnp ${⊢}{\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)={F}\left({X}\right)$