Metamath Proof Explorer


Theorem fourierdlem113

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

Ref Expression
Hypotheses fourierdlem113.f φ F :
fourierdlem113.t T = 2 π
fourierdlem113.per φ x F x + T = F x
fourierdlem113.x φ X
fourierdlem113.l φ L F −∞ X lim X
fourierdlem113.r φ R F X +∞ lim X
fourierdlem113.p P = n p 0 n | p 0 = π p n = π i 0 ..^ n p i < p i + 1
fourierdlem113.m φ M
fourierdlem113.q φ Q P M
fourierdlem113.dvcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
fourierdlem113.dvlb φ i 0 ..^ M F Q i Q i + 1 lim Q i
fourierdlem113.dvub φ i 0 ..^ M F Q i Q i + 1 lim Q i + 1
fourierdlem113.a A = n 0 π π F x cos n x dx π
fourierdlem113.b B = n π π F x sin n x dx π
fourierdlem113.15 S = n A n cos n X + B n sin n X
fourierdlem113.e E = x x + π x T T
fourierdlem113.exq φ E X ran Q
Assertion fourierdlem113 φ seq 1 + S L + R 2 A 0 2 A 0 2 + n A n cos n X + B n sin n X = L + R 2

Proof

Step Hyp Ref Expression
1 fourierdlem113.f φ F :
2 fourierdlem113.t T = 2 π
3 fourierdlem113.per φ x F x + T = F x
4 fourierdlem113.x φ X
5 fourierdlem113.l φ L F −∞ X lim X
6 fourierdlem113.r φ R F X +∞ lim X
7 fourierdlem113.p P = n p 0 n | p 0 = π p n = π i 0 ..^ n p i < p i + 1
8 fourierdlem113.m φ M
9 fourierdlem113.q φ Q P M
10 fourierdlem113.dvcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
11 fourierdlem113.dvlb φ i 0 ..^ M F Q i Q i + 1 lim Q i
12 fourierdlem113.dvub φ i 0 ..^ M F Q i Q i + 1 lim Q i + 1
13 fourierdlem113.a A = n 0 π π F x cos n x dx π
14 fourierdlem113.b B = n π π F x sin n x dx π
15 fourierdlem113.15 S = n A n cos n X + B n sin n X
16 fourierdlem113.e E = x x + π x T T
17 fourierdlem113.exq φ E X ran Q
18 oveq1 w = y w mod 2 π = y mod 2 π
19 18 eqeq1d w = y w mod 2 π = 0 y mod 2 π = 0
20 oveq2 w = y k + 1 2 w = k + 1 2 y
21 20 fveq2d w = y sin k + 1 2 w = sin k + 1 2 y
22 oveq1 w = y w 2 = y 2
23 22 fveq2d w = y sin w 2 = sin y 2
24 23 oveq2d w = y 2 π sin w 2 = 2 π sin y 2
25 21 24 oveq12d w = y sin k + 1 2 w 2 π sin w 2 = sin k + 1 2 y 2 π sin y 2
26 19 25 ifbieq2d w = y if w mod 2 π = 0 2 k + 1 2 π sin k + 1 2 w 2 π sin w 2 = if y mod 2 π = 0 2 k + 1 2 π sin k + 1 2 y 2 π sin y 2
27 26 cbvmptv w if w mod 2 π = 0 2 k + 1 2 π sin k + 1 2 w 2 π sin w 2 = y if y mod 2 π = 0 2 k + 1 2 π sin k + 1 2 y 2 π sin y 2
28 oveq2 k = m 2 k = 2 m
29 28 oveq1d k = m 2 k + 1 = 2 m + 1
30 29 oveq1d k = m 2 k + 1 2 π = 2 m + 1 2 π
31 oveq1 k = m k + 1 2 = m + 1 2
32 31 oveq1d k = m k + 1 2 y = m + 1 2 y
33 32 fveq2d k = m sin k + 1 2 y = sin m + 1 2 y
34 33 oveq1d k = m sin k + 1 2 y 2 π sin y 2 = sin m + 1 2 y 2 π sin y 2
35 30 34 ifeq12d k = m if y mod 2 π = 0 2 k + 1 2 π sin k + 1 2 y 2 π sin y 2 = if y mod 2 π = 0 2 m + 1 2 π sin m + 1 2 y 2 π sin y 2
36 35 mpteq2dv k = m y if y mod 2 π = 0 2 k + 1 2 π sin k + 1 2 y 2 π sin y 2 = y if y mod 2 π = 0 2 m + 1 2 π sin m + 1 2 y 2 π sin y 2
37 27 36 syl5eq k = m w if w mod 2 π = 0 2 k + 1 2 π sin k + 1 2 w 2 π sin w 2 = y if y mod 2 π = 0 2 m + 1 2 π sin m + 1 2 y 2 π sin y 2
38 37 cbvmptv k w if w mod 2 π = 0 2 k + 1 2 π sin k + 1 2 w 2 π sin w 2 = m y if y mod 2 π = 0 2 m + 1 2 π sin m + 1 2 y 2 π sin y 2
39 oveq1 w = y w + j T = y + j T
40 39 eleq1d w = y w + j T ran Q y + j T ran Q
41 40 rexbidv w = y j w + j T ran Q j y + j T ran Q
42 41 cbvrabv w - π + X π + X | j w + j T ran Q = y - π + X π + X | j y + j T ran Q
43 42 uneq2i - π + X π + X w - π + X π + X | j w + j T ran Q = - π + X π + X y - π + X π + X | j y + j T ran Q
44 43 fveq2i - π + X π + X w - π + X π + X | j w + j T ran Q = - π + X π + X y - π + X π + X | j y + j T ran Q
45 44 oveq1i - π + X π + X w - π + X π + X | j w + j T ran Q 1 = - π + X π + X y - π + X π + X | j y + j T ran Q 1
46 oveq1 k = j k T = j T
47 46 oveq2d k = j y + k T = y + j T
48 47 eleq1d k = j y + k T ran Q y + j T ran Q
49 48 cbvrexvw k y + k T ran Q j y + j T ran Q
50 49 a1i y - π + X π + X k y + k T ran Q j y + j T ran Q
51 50 rabbiia y - π + X π + X | k y + k T ran Q = y - π + X π + X | j y + j T ran Q
52 51 uneq2i - π + X π + X y - π + X π + X | k y + k T ran Q = - π + X π + X y - π + X π + X | j y + j T ran Q
53 isoeq5 - π + X π + X y - π + X π + X | k y + k T ran Q = - π + X π + X y - π + X π + X | j y + j T ran Q g Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q g Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | j y + j T ran Q
54 52 53 ax-mp g Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q g Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | j y + j T ran Q
55 54 a1i g = f g Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q g Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | j y + j T ran Q
56 46 oveq2d k = j w + k T = w + j T
57 56 eleq1d k = j w + k T ran Q w + j T ran Q
58 57 cbvrexvw k w + k T ran Q j w + j T ran Q
59 58 a1i w - π + X π + X k w + k T ran Q j w + j T ran Q
60 59 rabbiia w - π + X π + X | k w + k T ran Q = w - π + X π + X | j w + j T ran Q
61 60 uneq2i - π + X π + X w - π + X π + X | k w + k T ran Q = - π + X π + X w - π + X π + X | j w + j T ran Q
62 61 fveq2i - π + X π + X w - π + X π + X | k w + k T ran Q = - π + X π + X w - π + X π + X | j w + j T ran Q
63 62 oveq1i - π + X π + X w - π + X π + X | k w + k T ran Q 1 = - π + X π + X w - π + X π + X | j w + j T ran Q 1
64 63 oveq2i 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 = 0 - π + X π + X w - π + X π + X | j w + j T ran Q 1
65 isoeq4 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 = 0 - π + X π + X w - π + X π + X | j w + j T ran Q 1 g Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | j y + j T ran Q g Isom < , < 0 - π + X π + X w - π + X π + X | j w + j T ran Q 1 - π + X π + X y - π + X π + X | j y + j T ran Q
66 64 65 ax-mp g Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | j y + j T ran Q g Isom < , < 0 - π + X π + X w - π + X π + X | j w + j T ran Q 1 - π + X π + X y - π + X π + X | j y + j T ran Q
67 66 a1i g = f g Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | j y + j T ran Q g Isom < , < 0 - π + X π + X w - π + X π + X | j w + j T ran Q 1 - π + X π + X y - π + X π + X | j y + j T ran Q
68 isoeq1 g = f g Isom < , < 0 - π + X π + X w - π + X π + X | j w + j T ran Q 1 - π + X π + X y - π + X π + X | j y + j T ran Q f Isom < , < 0 - π + X π + X w - π + X π + X | j w + j T ran Q 1 - π + X π + X y - π + X π + X | j y + j T ran Q
69 55 67 68 3bitrd g = f g Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q f Isom < , < 0 - π + X π + X w - π + X π + X | j w + j T ran Q 1 - π + X π + X y - π + X π + X | j y + j T ran Q
70 69 cbviotavw ι g | g Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q = ι f | f Isom < , < 0 - π + X π + X w - π + X π + X | j w + j T ran Q 1 - π + X π + X y - π + X π + X | j y + j T ran Q
71 pire π
72 71 renegcli π
73 72 a1i φ π
74 71 a1i φ π
75 negpilt0 π < 0
76 75 a1i φ π < 0
77 pipos 0 < π
78 77 a1i φ 0 < π
79 picn π
80 79 2timesi 2 π = π + π
81 79 79 subnegi π π = π + π
82 80 2 81 3eqtr4i T = π π
83 7 fourierdlem2 M Q P M Q 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
84 8 83 syl φ Q P M Q 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
85 9 84 mpbid φ Q 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
86 85 simpld φ Q 0 M
87 elmapi Q 0 M Q : 0 M
88 86 87 syl φ Q : 0 M
89 fzfid φ 0 M Fin
90 rnffi Q : 0 M 0 M Fin ran Q Fin
91 88 89 90 syl2anc φ ran Q Fin
92 7 8 9 fourierdlem15 φ Q : 0 M π π
93 frn Q : 0 M π π ran Q π π
94 92 93 syl φ ran Q π π
95 85 simprd φ Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
96 95 simplrd φ Q M = π
97 ffun Q : 0 M π π Fun Q
98 92 97 syl φ Fun Q
99 8 nnnn0d φ M 0
100 nn0uz 0 = 0
101 99 100 eleqtrdi φ M 0
102 eluzfz2 M 0 M 0 M
103 101 102 syl φ M 0 M
104 fdm Q : 0 M π π dom Q = 0 M
105 92 104 syl φ dom Q = 0 M
106 105 eqcomd φ 0 M = dom Q
107 103 106 eleqtrd φ M dom Q
108 fvelrn Fun Q M dom Q Q M ran Q
109 98 107 108 syl2anc φ Q M ran Q
110 96 109 eqeltrrd φ π ran Q
111 eqid - π + X π + X w - π + X π + X | k w + k T ran Q = - π + X π + X w - π + X π + X | k w + k T ran Q
112 isoeq1 g = f g Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q f Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q
113 43 61 52 3eqtr4ri - π + X π + X y - π + X π + X | k y + k T ran Q = - π + X π + X w - π + X π + X | k w + k T ran Q
114 isoeq5 - π + X π + X y - π + X π + X | k y + k T ran Q = - π + X π + X w - π + X π + X | k w + k T ran Q f Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q f Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X w - π + X π + X | k w + k T ran Q
115 113 114 ax-mp f Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q f Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X w - π + X π + X | k w + k T ran Q
116 112 115 bitrdi g = f g Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q f Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X w - π + X π + X | k w + k T ran Q
117 116 cbviotavw ι g | g Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q = ι f | f Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X w - π + X π + X | k w + k T ran Q
118 eqid w - π + X π + X | k w + k T ran Q = w - π + X π + X | k w + k T ran Q
119 73 74 76 78 82 91 94 110 16 4 17 111 117 118 fourierdlem51 φ X ran ι g | g Isom < , < 0 - π + X π + X w - π + X π + X | k w + k T ran Q 1 - π + X π + X y - π + X π + X | k y + k T ran Q
120 ax-resscn
121 120 a1i φ i 0 ..^ M
122 ioossre Q i Q i + 1
123 122 a1i φ Q i Q i + 1
124 1 123 fssresd φ F Q i Q i + 1 : Q i Q i + 1
125 120 a1i φ
126 124 125 fssd φ F Q i Q i + 1 : Q i Q i + 1
127 126 adantr φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1
128 122 a1i φ i 0 ..^ M Q i Q i + 1
129 1 125 fssd φ F :
130 129 adantr φ i 0 ..^ M F :
131 ssid
132 131 a1i φ i 0 ..^ M
133 eqid TopOpen fld = TopOpen fld
134 133 tgioo2 topGen ran . = TopOpen fld 𝑡
135 133 134 dvres F : Q i Q i + 1 D F Q i Q i + 1 = F int topGen ran . Q i Q i + 1
136 121 130 132 128 135 syl22anc φ i 0 ..^ M D F Q i Q i + 1 = F int topGen ran . Q i Q i + 1
137 136 dmeqd φ i 0 ..^ M dom F Q i Q i + 1 = dom F int topGen ran . Q i Q i + 1
138 ioontr int topGen ran . Q i Q i + 1 = Q i Q i + 1
139 138 reseq2i F int topGen ran . Q i Q i + 1 = F Q i Q i + 1
140 139 dmeqi dom F int topGen ran . Q i Q i + 1 = dom F Q i Q i + 1
141 140 a1i φ i 0 ..^ M dom F int topGen ran . Q i Q i + 1 = dom F Q i Q i + 1
142 cncff F Q i Q i + 1 : Q i Q i + 1 cn F Q i Q i + 1 : Q i Q i + 1
143 fdm F Q i Q i + 1 : Q i Q i + 1 dom F Q i Q i + 1 = Q i Q i + 1
144 10 142 143 3syl φ i 0 ..^ M dom F Q i Q i + 1 = Q i Q i + 1
145 137 141 144 3eqtrd φ i 0 ..^ M dom F Q i Q i + 1 = Q i Q i + 1
146 dvcn F Q i Q i + 1 : Q i Q i + 1 Q i Q i + 1 dom F Q i Q i + 1 = Q i Q i + 1 F Q i Q i + 1 : Q i Q i + 1 cn
147 121 127 128 145 146 syl31anc φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
148 128 121 sstrd φ i 0 ..^ M Q i Q i + 1
149 88 adantr φ i 0 ..^ M Q : 0 M
150 fzofzp1 i 0 ..^ M i + 1 0 M
151 150 adantl φ i 0 ..^ M i + 1 0 M
152 149 151 ffvelrnd φ i 0 ..^ M Q i + 1
153 152 rexrd φ i 0 ..^ M Q i + 1 *
154 elfzofz i 0 ..^ M i 0 M
155 154 adantl φ i 0 ..^ M i 0 M
156 149 155 ffvelrnd φ i 0 ..^ M Q i
157 85 simprrd φ i 0 ..^ M Q i < Q i + 1
158 157 r19.21bi φ i 0 ..^ M Q i < Q i + 1
159 133 153 156 158 lptioo1cn φ i 0 ..^ M Q i limPt TopOpen fld Q i Q i + 1
160 124 adantr φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1
161 131 a1i φ
162 125 129 161 dvbss φ dom F
163 dvfre F : F : dom F
164 1 161 163 syl2anc φ F : dom F
165 0re 0
166 72 165 71 lttri π < 0 0 < π π < π
167 75 77 166 mp2an π < π
168 167 a1i φ π < π
169 95 simplld φ Q 0 = π
170 10 142 syl φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1
171 170 148 159 11 133 ellimciota φ i 0 ..^ M ι x | x F Q i Q i + 1 lim Q i F Q i Q i + 1 lim Q i
172 156 rexrd φ i 0 ..^ M Q i *
173 133 172 152 158 lptioo2cn φ i 0 ..^ M Q i + 1 limPt TopOpen fld Q i Q i + 1
174 170 148 173 12 133 ellimciota φ i 0 ..^ M ι x | x F Q i Q i + 1 lim Q i + 1 F Q i Q i + 1 lim Q i + 1
175 129 adantr φ k F :
176 zre k k
177 176 adantl φ k k
178 2re 2
179 178 71 remulcli 2 π
180 179 a1i φ 2 π
181 2 180 eqeltrid φ T
182 181 adantr φ k T
183 177 182 remulcld φ k k T
184 175 adantr φ k t F :
185 182 adantr φ k t T
186 simplr φ k t k
187 simpr φ k t t
188 3 ad4ant14 φ k t x F x + T = F x
189 184 185 186 187 188 fperiodmul φ k t F t + k T = F t
190 eqid D F = D F
191 175 183 189 190 fperdvper φ k t dom F t + k T dom F F t + k T = F t
192 191 an32s φ t dom F k t + k T dom F F t + k T = F t
193 192 simpld φ t dom F k t + k T dom F
194 192 simprd φ t dom F k F t + k T = F t
195 fveq2 j = i Q j = Q i
196 oveq1 j = i j + 1 = i + 1
197 196 fveq2d j = i Q j + 1 = Q i + 1
198 195 197 oveq12d j = i Q j Q j + 1 = Q i Q i + 1
199 198 cbvmptv j 0 ..^ M Q j Q j + 1 = i 0 ..^ M Q i Q i + 1
200 eqid t t + π t T T = t t + π t T T
201 162 164 73 74 168 82 8 88 169 96 10 171 174 193 194 199 200 fourierdlem71 φ z t dom F F t z
202 201 adantr φ i 0 ..^ M z t dom F F t z
203 nfv t φ i 0 ..^ M
204 nfra1 t t dom F F t z
205 203 204 nfan t φ i 0 ..^ M t dom F F t z
206 136 139 eqtrdi φ i 0 ..^ M D F Q i Q i + 1 = F Q i Q i + 1
207 206 fveq1d φ i 0 ..^ M F Q i Q i + 1 t = F Q i Q i + 1 t
208 fvres t Q i Q i + 1 F Q i Q i + 1 t = F t
209 207 208 sylan9eq φ i 0 ..^ M t Q i Q i + 1 F Q i Q i + 1 t = F t
210 209 fveq2d φ i 0 ..^ M t Q i Q i + 1 F Q i Q i + 1 t = F t
211 210 adantlr φ i 0 ..^ M t dom F F t z t Q i Q i + 1 F Q i Q i + 1 t = F t
212 simplr φ i 0 ..^ M t dom F F t z t Q i Q i + 1 t dom F F t z
213 ssdmres Q i Q i + 1 dom F dom F Q i Q i + 1 = Q i Q i + 1
214 144 213 sylibr φ i 0 ..^ M Q i Q i + 1 dom F
215 214 ad2antrr φ i 0 ..^ M t dom F F t z t Q i Q i + 1 Q i Q i + 1 dom F
216 simpr φ i 0 ..^ M t dom F F t z t Q i Q i + 1 t Q i Q i + 1
217 215 216 sseldd φ i 0 ..^ M t dom F F t z t Q i Q i + 1 t dom F
218 rspa t dom F F t z t dom F F t z
219 212 217 218 syl2anc φ i 0 ..^ M t dom F F t z t Q i Q i + 1 F t z
220 211 219 eqbrtrd φ i 0 ..^ M t dom F F t z t Q i Q i + 1 F Q i Q i + 1 t z
221 220 ex φ i 0 ..^ M t dom F F t z t Q i Q i + 1 F Q i Q i + 1 t z
222 205 221 ralrimi φ i 0 ..^ M t dom F F t z t Q i Q i + 1 F Q i Q i + 1 t z
223 222 ex φ i 0 ..^ M t dom F F t z t Q i Q i + 1 F Q i Q i + 1 t z
224 223 reximdv φ i 0 ..^ M z t dom F F t z z t Q i Q i + 1 F Q i Q i + 1 t z
225 202 224 mpd φ i 0 ..^ M z t Q i Q i + 1 F Q i Q i + 1 t z
226 156 152 160 145 225 ioodvbdlimc1 φ i 0 ..^ M F Q i Q i + 1 lim Q i
227 127 148 159 226 133 ellimciota φ i 0 ..^ M ι y | y F Q i Q i + 1 lim Q i F Q i Q i + 1 lim Q i
228 156 152 160 145 225 ioodvbdlimc2 φ i 0 ..^ M F Q i Q i + 1 lim Q i + 1
229 127 148 173 228 133 ellimciota φ i 0 ..^ M ι y | y F Q i Q i + 1 lim Q i + 1 F Q i Q i + 1 lim Q i + 1
230 frel F : dom F Rel F
231 164 230 syl φ Rel F
232 resindm Rel F F −∞ X dom F = F −∞ X
233 231 232 syl φ F −∞ X dom F = F −∞ X
234 inss2 −∞ X dom F dom F
235 234 a1i φ −∞ X dom F dom F
236 164 235 fssresd φ F −∞ X dom F : −∞ X dom F
237 233 236 feq1dd φ F −∞ X : −∞ X dom F
238 237 125 fssd φ F −∞ X : −∞ X dom F
239 ioosscn −∞ X
240 ssinss1 −∞ X −∞ X dom F
241 239 240 ax-mp −∞ X dom F
242 241 a1i φ −∞ X dom F
243 3simpb φ x dom F k φ k
244 simp2 φ x dom F k x dom F
245 175 adantr φ k x F :
246 182 adantr φ k x T
247 simplr φ k x k
248 simpr φ k x x
249 eleq1w x = y x y
250 249 anbi2d x = y φ x φ y
251 oveq1 x = y x + T = y + T
252 251 fveq2d x = y F x + T = F y + T
253 fveq2 x = y F x = F y
254 252 253 eqeq12d x = y F x + T = F x F y + T = F y
255 250 254 imbi12d x = y φ x F x + T = F x φ y F y + T = F y
256 255 3 chvarvv φ y F y + T = F y
257 256 ad4ant14 φ k x y F y + T = F y
258 245 246 247 248 257 fperiodmul φ k x F x + k T = F x
259 175 183 258 190 fperdvper φ k x dom F x + k T dom F F x + k T = F x
260 243 244 259 syl2anc φ x dom F k x + k T dom F F x + k T = F x
261 260 simpld φ x dom F k x + k T dom F
262 oveq2 w = x π w = π x
263 262 oveq1d w = x π w T = π x T
264 263 fveq2d w = x π w T = π x T
265 264 oveq1d w = x π w T T = π x T T
266 265 cbvmptv w π w T T = x π x T T
267 eqid x x + w π w T T x = x x + w π w T T x
268 73 74 168 82 261 4 266 267 7 8 9 214 fourierdlem41 φ y y < X y X dom F y X < y X y dom F
269 268 simpld φ y y < X y X dom F
270 133 cnfldtop TopOpen fld Top
271 270 a1i φ y y X dom F TopOpen fld Top
272 241 a1i φ y y X dom F −∞ X dom F
273 mnfxr −∞ *
274 273 a1i y −∞ *
275 rexr y y *
276 mnflt y −∞ < y
277 274 275 276 xrltled y −∞ y
278 iooss1 −∞ * −∞ y y X −∞ X
279 274 277 278 syl2anc y y X −∞ X
280 279 3ad2ant2 φ y y X dom F y X −∞ X
281 simp3 φ y y X dom F y X dom F
282 280 281 ssind φ y y X dom F y X −∞ X dom F
283 unicntop = TopOpen fld
284 283 lpss3 TopOpen fld Top −∞ X dom F y X −∞ X dom F limPt TopOpen fld y X limPt TopOpen fld −∞ X dom F
285 271 272 282 284 syl3anc φ y y X dom F limPt TopOpen fld y X limPt TopOpen fld −∞ X dom F
286 285 3adant3l φ y y < X y X dom F limPt TopOpen fld y X limPt TopOpen fld −∞ X dom F
287 275 3ad2ant2 φ y y < X y X dom F y *
288 4 3ad2ant1 φ y y < X y X dom F X
289 simp3l φ y y < X y X dom F y < X
290 133 287 288 289 lptioo2cn φ y y < X y X dom F X limPt TopOpen fld y X
291 286 290 sseldd φ y y < X y X dom F X limPt TopOpen fld −∞ X dom F
292 291 rexlimdv3a φ y y < X y X dom F X limPt TopOpen fld −∞ X dom F
293 269 292 mpd φ X limPt TopOpen fld −∞ X dom F
294 260 simprd φ x dom F k F x + k T = F x
295 oveq2 y = x π y = π x
296 295 oveq1d y = x π y T = π x T
297 296 fveq2d y = x π y T = π x T
298 297 oveq1d y = x π y T T = π x T T
299 298 cbvmptv y π y T T = x π x T T
300 id z = x z = x
301 fveq2 z = x y π y T T z = y π y T T x
302 300 301 oveq12d z = x z + y π y T T z = x + y π y T T x
303 302 cbvmptv z z + y π y T T z = x x + y π y T T x
304 73 74 168 7 82 8 9 162 164 261 294 10 174 4 299 303 fourierdlem49 φ F −∞ X lim X
305 238 242 293 304 133 ellimciota φ ι x | x F −∞ X lim X F −∞ X lim X
306 resindm Rel F F X +∞ dom F = F X +∞
307 231 306 syl φ F X +∞ dom F = F X +∞
308 inss2 X +∞ dom F dom F
309 308 a1i φ X +∞ dom F dom F
310 164 309 fssresd φ F X +∞ dom F : X +∞ dom F
311 307 310 feq1dd φ F X +∞ : X +∞ dom F
312 311 125 fssd φ F X +∞ : X +∞ dom F
313 ioosscn X +∞
314 ssinss1 X +∞ X +∞ dom F
315 313 314 ax-mp X +∞ dom F
316 315 a1i φ X +∞ dom F
317 268 simprd φ y X < y X y dom F
318 270 a1i φ y X y dom F TopOpen fld Top
319 315 a1i φ y X y dom F X +∞ dom F
320 pnfxr +∞ *
321 320 a1i y +∞ *
322 ltpnf y y < +∞
323 275 321 322 xrltled y y +∞
324 iooss2 +∞ * y +∞ X y X +∞
325 321 323 324 syl2anc y X y X +∞
326 325 3ad2ant2 φ y X y dom F X y X +∞
327 simp3 φ y X y dom F X y dom F
328 326 327 ssind φ y X y dom F X y X +∞ dom F
329 283 lpss3 TopOpen fld Top X +∞ dom F X y X +∞ dom F limPt TopOpen fld X y limPt TopOpen fld X +∞ dom F
330 318 319 328 329 syl3anc φ y X y dom F limPt TopOpen fld X y limPt TopOpen fld X +∞ dom F
331 330 3adant3l φ y X < y X y dom F limPt TopOpen fld X y limPt TopOpen fld X +∞ dom F
332 275 3ad2ant2 φ y X < y X y dom F y *
333 4 3ad2ant1 φ y X < y X y dom F X
334 simp3l φ y X < y X y dom F X < y
335 133 332 333 334 lptioo1cn φ y X < y X y dom F X limPt TopOpen fld X y
336 331 335 sseldd φ y X < y X y dom F X limPt TopOpen fld X +∞ dom F
337 336 rexlimdv3a φ y X < y X y dom F X limPt TopOpen fld X +∞ dom F
338 317 337 mpd φ X limPt TopOpen fld X +∞ dom F
339 biid φ i 0 ..^ M w Q i Q i + 1 k w = X + k T φ i 0 ..^ M w Q i Q i + 1 k w = X + k T
340 73 74 168 7 82 8 9 164 261 294 10 171 4 299 303 339 fourierdlem48 φ F X +∞ lim X
341 312 316 338 340 133 ellimciota φ ι x | x F X +∞ lim X F X +∞ lim X
342 fveq2 n = k A n = A k
343 oveq1 n = k n X = k X
344 343 fveq2d n = k cos n X = cos k X
345 342 344 oveq12d n = k A n cos n X = A k cos k X
346 fveq2 n = k B n = B k
347 343 fveq2d n = k sin n X = sin k X
348 346 347 oveq12d n = k B n sin n X = B k sin k X
349 345 348 oveq12d n = k A n cos n X + B n sin n X = A k cos k X + B k sin k X
350 349 cbvsumv n = 1 m A n cos n X + B n sin n X = k = 1 m A k cos k X + B k sin k X
351 oveq2 j = m 1 j = 1 m
352 351 eqcomd j = m 1 m = 1 j
353 352 sumeq1d j = m k = 1 m A k cos k X + B k sin k X = k = 1 j A k cos k X + B k sin k X
354 350 353 eqtr2id j = m k = 1 j A k cos k X + B k sin k X = n = 1 m A n cos n X + B n sin n X
355 354 oveq2d j = m A 0 2 + k = 1 j A k cos k X + B k sin k X = A 0 2 + n = 1 m A n cos n X + B n sin n X
356 355 cbvmptv j A 0 2 + k = 1 j A k cos k X + B k sin k X = m A 0 2 + n = 1 m A n cos n X + B n sin n X
357 fdm F : dom F =
358 1 357 syl φ dom F =
359 358 161 eqsstrd φ dom F
360 358 feq2d φ F : dom F F :
361 1 360 mpbird φ F : dom F
362 359 sselda φ t dom F t
363 362 adantr φ t dom F k t
364 176 adantl φ t dom F k k
365 182 adantlr φ t dom F k T
366 364 365 remulcld φ t dom F k k T
367 363 366 readdcld φ t dom F k t + k T
368 358 eqcomd φ = dom F
369 368 ad2antrr φ t dom F k = dom F
370 367 369 eleqtrd φ t dom F k t + k T dom F
371 id φ k φ k
372 371 adantlr φ t dom F k φ k
373 372 363 189 syl2anc φ t dom F k F t + k T = F t
374 359 361 73 74 168 82 8 88 169 96 147 227 229 370 373 199 200 fourierdlem71 φ u t dom F F t u
375 358 raleqdv φ t dom F F t u t F t u
376 375 rexbidv φ u t dom F F t u u t F t u
377 374 376 mpbid φ u t F t u
378 1 38 7 8 9 45 70 4 119 2 3 147 227 229 10 305 341 5 6 13 14 356 15 377 201 4 fourierdlem112 φ seq 1 + S L + R 2 A 0 2 A 0 2 + n A n cos n X + B n sin n X = L + R 2