# Metamath Proof Explorer

## Theorem fouriercnp

Description: If F is continuous at the point X , then its Fourier series at X , converges to ( FX ) . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fouriercnp.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
fouriercnp.t ${⊢}{T}=2\mathrm{\pi }$
fouriercnp.per ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)$
fouriercnp.g ${⊢}{G}={{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}$
fouriercnp.dmdv ${⊢}{\phi }\to \left(-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}{G}\in \mathrm{Fin}$
fouriercnp.dvcn ${⊢}{\phi }\to {G}:\mathrm{dom}{G}\underset{cn}{⟶}ℂ$
fouriercnp.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$
fouriercnp.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$
fouriercnp.j ${⊢}{J}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
fouriercnp.cnp ${⊢}{\phi }\to {F}\in \left({J}\mathrm{CnP}{J}\right)\left({X}\right)$
fouriercnp.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)$
fouriercnp.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 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)$

### Proof

Step Hyp Ref Expression
1 fouriercnp.f ${⊢}{\phi }\to {F}:ℝ⟶ℝ$
2 fouriercnp.t ${⊢}{T}=2\mathrm{\pi }$
3 fouriercnp.per ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)$
4 fouriercnp.g ${⊢}{G}={{{F}}_{ℝ}^{\prime }↾}_{\left(-\mathrm{\pi },\mathrm{\pi }\right)}$
5 fouriercnp.dmdv ${⊢}{\phi }\to \left(-\mathrm{\pi },\mathrm{\pi }\right)\setminus \mathrm{dom}{G}\in \mathrm{Fin}$
6 fouriercnp.dvcn ${⊢}{\phi }\to {G}:\mathrm{dom}{G}\underset{cn}{⟶}ℂ$
7 fouriercnp.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 fouriercnp.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 fouriercnp.j ${⊢}{J}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
10 fouriercnp.cnp ${⊢}{\phi }\to {F}\in \left({J}\mathrm{CnP}{J}\right)\left({X}\right)$
11 fouriercnp.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)$
12 fouriercnp.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)$
13 uniretop ${⊢}ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
14 9 unieqi ${⊢}\bigcup {J}=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
15 13 14 eqtr4i ${⊢}ℝ=\bigcup {J}$
16 15 cnprcl ${⊢}{F}\in \left({J}\mathrm{CnP}{J}\right)\left({X}\right)\to {X}\in ℝ$
17 10 16 syl ${⊢}{\phi }\to {X}\in ℝ$
18 limcresi ${⊢}{F}{lim}_{ℂ}{X}\subseteq \left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}$
19 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
20 19 tgioo2 ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
21 9 20 eqtri ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
22 21 oveq2i ${⊢}{J}\mathrm{CnP}{J}={J}\mathrm{CnP}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)$
23 22 fveq1i ${⊢}\left({J}\mathrm{CnP}{J}\right)\left({X}\right)=\left({J}\mathrm{CnP}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)\left({X}\right)$
24 10 23 eleqtrdi ${⊢}{\phi }\to {F}\in \left({J}\mathrm{CnP}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)\left({X}\right)$
25 19 cnfldtop ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}$
26 25 a1i ${⊢}{\phi }\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}$
27 ax-resscn ${⊢}ℝ\subseteq ℂ$
28 27 a1i ${⊢}{\phi }\to ℝ\subseteq ℂ$
29 unicntop ${⊢}ℂ=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
30 15 29 cnprest2 ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}\wedge {F}:ℝ⟶ℝ\wedge ℝ\subseteq ℂ\right)\to \left({F}\in \left({J}\mathrm{CnP}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left({X}\right)↔{F}\in \left({J}\mathrm{CnP}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)\left({X}\right)\right)$
31 26 1 28 30 syl3anc ${⊢}{\phi }\to \left({F}\in \left({J}\mathrm{CnP}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left({X}\right)↔{F}\in \left({J}\mathrm{CnP}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ\right)\right)\left({X}\right)\right)$
32 24 31 mpbird ${⊢}{\phi }\to {F}\in \left({J}\mathrm{CnP}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left({X}\right)$
33 19 21 cnplimc ${⊢}\left(ℝ\subseteq ℂ\wedge {X}\in ℝ\right)\to \left({F}\in \left({J}\mathrm{CnP}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left({X}\right)↔\left({F}:ℝ⟶ℂ\wedge {F}\left({X}\right)\in \left({F}{lim}_{ℂ}{X}\right)\right)\right)$
34 27 17 33 sylancr ${⊢}{\phi }\to \left({F}\in \left({J}\mathrm{CnP}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left({X}\right)↔\left({F}:ℝ⟶ℂ\wedge {F}\left({X}\right)\in \left({F}{lim}_{ℂ}{X}\right)\right)\right)$
35 32 34 mpbid ${⊢}{\phi }\to \left({F}:ℝ⟶ℂ\wedge {F}\left({X}\right)\in \left({F}{lim}_{ℂ}{X}\right)\right)$
36 35 simprd ${⊢}{\phi }\to {F}\left({X}\right)\in \left({F}{lim}_{ℂ}{X}\right)$
37 18 36 sseldi ${⊢}{\phi }\to {F}\left({X}\right)\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{X}\right)}\right){lim}_{ℂ}{X}\right)$
38 limcresi ${⊢}{F}{lim}_{ℂ}{X}\subseteq \left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}$
39 38 36 sseldi ${⊢}{\phi }\to {F}\left({X}\right)\in \left(\left({{F}↾}_{\left({X},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{X}\right)$
40 1 2 3 4 5 6 7 8 17 37 39 11 12 fourierd ${⊢}{\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{{F}\left({X}\right)+{F}\left({X}\right)}{2}$
41 1 17 ffvelrnd ${⊢}{\phi }\to {F}\left({X}\right)\in ℝ$
42 41 recnd ${⊢}{\phi }\to {F}\left({X}\right)\in ℂ$
43 42 2timesd ${⊢}{\phi }\to 2{F}\left({X}\right)={F}\left({X}\right)+{F}\left({X}\right)$
44 43 eqcomd ${⊢}{\phi }\to {F}\left({X}\right)+{F}\left({X}\right)=2{F}\left({X}\right)$
45 44 oveq1d ${⊢}{\phi }\to \frac{{F}\left({X}\right)+{F}\left({X}\right)}{2}=\frac{2{F}\left({X}\right)}{2}$
46 2cnd ${⊢}{\phi }\to 2\in ℂ$
47 2ne0 ${⊢}2\ne 0$
48 47 a1i ${⊢}{\phi }\to 2\ne 0$
49 42 46 48 divcan3d ${⊢}{\phi }\to \frac{2{F}\left({X}\right)}{2}={F}\left({X}\right)$
50 40 45 49 3eqtrd ${⊢}{\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)$