Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem112 Structured version   Unicode version

Theorem fourierdlem112 31842
 Description: Here abbreviations (local definitions) are introduced to prove the fourier 31849 theorem. is the mth partial sum of the fourier series. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem112.f
fourierdlem112.d
fourierdlem112.p ..^
fourierdlem112.m
fourierdlem112.q
fourierdlem112.n
fourierdlem112.v
fourierdlem112.x
fourierdlem112.xran
fourierdlem112.t
fourierdlem112.fper
fourierdlem112.fcn ..^
fourierdlem112.c ..^ lim
fourierdlem112.u ..^ lim
fourierdlem112.fdvcn ..^
fourierdlem112.e lim
fourierdlem112.i lim
fourierdlem112.l lim
fourierdlem112.r lim
fourierdlem112.a
fourierdlem112.b
fourierdlem112.z
fourierdlem112.23
fourierdlem112.fbd
fourierdlem112.fdvbd
fourierdlem112.25
Assertion
Ref Expression
fourierdlem112
Distinct variable groups:   ,,,   ,,,   ,,   ,,   ,,,,,,   ,,,   ,,,,   ,,   ,   ,,,,   ,   ,,,,,   ,   ,   ,,,,,   ,,   ,,,,   ,,,,   ,,,   ,,   ,,   ,,,,,,   ,,   ,,   ,,,,,   ,   ,   ,,,,,,   ,,   ,   ,,   ,   ,,,,   ,,,   ,,   ,   ,,,   ,,,,   ,,   ,   ,   ,   ,,,,   ,,,,   ,   ,   ,
Allowed substitution hints:   ()   (,,,,,,,)   (,,,,,,,)   (,,,,,,,)   (,,,,)   (,,,,,,,,,,)   (,)   (,,,)   (,,,,,,,,,,)   (,)   (,,,,,,,)   (,,,,,,,,,,)   (,)   (,,,,,,,,,,)   (,,,)   (,,)   ()   ()   (,,,,,,,,,)

Proof of Theorem fourierdlem112
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem112.23 . . . . . 6
2 fveq2 5872 . . . . . . . . 9
3 oveq1 6302 . . . . . . . . . 10
43fveq2d 5876 . . . . . . . . 9
52, 4oveq12d 6313 . . . . . . . 8
6 fveq2 5872 . . . . . . . . 9
73fveq2d 5876 . . . . . . . . 9
86, 7oveq12d 6313 . . . . . . . 8
95, 8oveq12d 6313 . . . . . . 7
109cbvmptv 4544 . . . . . 6
111, 10eqtri 2496 . . . . 5
12 seqeq3 12092 . . . . 5
1311, 12ax-mp 5 . . . 4
1413a1i 11 . . 3
15 nnuz 11129 . . . . 5
16 1z 10906 . . . . . 6
1716a1i 11 . . . . 5
18 nfv 1683 . . . . . . 7
19 nfcv 2629 . . . . . . . 8
20 nfcv 2629 . . . . . . . . 9
21 nfcv 2629 . . . . . . . . . 10
22 nfcv 2629 . . . . . . . . . 10
23 nfcv 2629 . . . . . . . . . 10
2421, 22, 23nfov 6318 . . . . . . . . 9
2520, 24nfitg 22049 . . . . . . . 8
2619, 25nfmpt 4541 . . . . . . 7
27 nfcv 2629 . . . . . . . . 9
2827, 24nfitg 22049 . . . . . . . 8
2919, 28nfmpt 4541 . . . . . . 7
30 fourierdlem112.z . . . . . . . 8
31 fourierdlem112.a . . . . . . . . . . . . 13
32 nfmpt1 4542 . . . . . . . . . . . . 13
3331, 32nfcxfr 2627 . . . . . . . . . . . 12
34 nfcv 2629 . . . . . . . . . . . 12
3533, 34nffv 5879 . . . . . . . . . . 11
36 nfcv 2629 . . . . . . . . . . 11
37 nfcv 2629 . . . . . . . . . . 11
3835, 36, 37nfov 6318 . . . . . . . . . 10
39 nfcv 2629 . . . . . . . . . 10
40 nfcv 2629 . . . . . . . . . . 11
4140nfsum1 13492 . . . . . . . . . 10
4238, 39, 41nfov 6318 . . . . . . . . 9
4319, 42nfmpt 4541 . . . . . . . 8
4430, 43nfcxfr 2627 . . . . . . 7
45 fourierdlem112.f . . . . . . . 8
46 fourierdlem112.25 . . . . . . . 8
47 eqid 2467 . . . . . . . 8 ..^ ..^
48 ax-resscn 9561 . . . . . . . . . . . . . 14
49 pire 22718 . . . . . . . . . . . . . 14
5048, 49sselii 3506 . . . . . . . . . . . . 13
51 subneg 9880 . . . . . . . . . . . . 13
5250, 50, 51mp2an 672 . . . . . . . . . . . 12
53502timesi 10668 . . . . . . . . . . . . 13
5453eqcomi 2480 . . . . . . . . . . . 12
55 fourierdlem112.t . . . . . . . . . . . . 13
5655eqcomi 2480 . . . . . . . . . . . 12
5752, 54, 563eqtrri 2501 . . . . . . . . . . 11
58 fourierdlem112.p . . . . . . . . . . 11 ..^
59 fourierdlem112.m . . . . . . . . . . 11
60 fourierdlem112.q . . . . . . . . . . 11
6149a1i 11 . . . . . . . . . . . . 13
6261renegcld 9998 . . . . . . . . . . . 12
6362, 46readdcld 9635 . . . . . . . . . . 11
6461, 46readdcld 9635 . . . . . . . . . . 11
65 negpilt0 31362 . . . . . . . . . . . . . 14
66 pipos 22720 . . . . . . . . . . . . . 14
6749renegcli 9892 . . . . . . . . . . . . . . 15
68 0re 9608 . . . . . . . . . . . . . . 15
6967, 68, 49lttri 9722 . . . . . . . . . . . . . 14
7065, 66, 69mp2an 672 . . . . . . . . . . . . 13
7170a1i 11 . . . . . . . . . . . 12
7262, 61, 46, 71ltadd1dd 10175 . . . . . . . . . . 11
73 oveq1 6302 . . . . . . . . . . . . . . 15
7473eleq1d 2536 . . . . . . . . . . . . . 14
7574rexbidv 2978 . . . . . . . . . . . . 13
7675cbvrabv 3117 . . . . . . . . . . . 12
7776uneq2i 3660 . . . . . . . . . . 11
78 fourierdlem112.n . . . . . . . . . . 11
79 fourierdlem112.v . . . . . . . . . . 11
8057, 58, 59, 60, 63, 64, 72, 47, 77, 78, 79fourierdlem54 31784 . . . . . . . . . 10 ..^
8180simpld 459 . . . . . . . . 9 ..^
8281simpld 459 . . . . . . . 8
8381simprd 463 . . . . . . . 8 ..^
84 fourierdlem112.xran . . . . . . . 8
8545adantr 465 . . . . . . . . 9 ..^
86 fveq2 5872 . . . . . . . . . . . . . . . 16
87 oveq1 6302 . . . . . . . . . . . . . . . . 17
8887fveq2d 5876 . . . . . . . . . . . . . . . 16
8986, 88breq12d 4466 . . . . . . . . . . . . . . 15
9089cbvralv 3093 . . . . . . . . . . . . . 14 ..^ ..^
9190anbi2i 694 . . . . . . . . . . . . 13 ..^ ..^
9291a1i 11 . . . . . . . . . . . 12 ..^ ..^
9392rabbiia 3107 . . . . . . . . . . 11 ..^ ..^
9493mpteq2i 4536 . . . . . . . . . 10 ..^ ..^
9558, 94eqtri 2496 . . . . . . . . 9 ..^
9659adantr 465 . . . . . . . . 9 ..^
9760adantr 465 . . . . . . . . 9 ..^
98 fourierdlem112.fper . . . . . . . . . 10
9998adantlr 714 . . . . . . . . 9 ..^
100 eleq1 2539 . . . . . . . . . . . . 13 ..^ ..^
101100anbi2d 703 . . . . . . . . . . . 12 ..^ ..^
102 fveq2 5872 . . . . . . . . . . . . . . 15
10387fveq2d 5876 . . . . . . . . . . . . . . 15
104102, 103oveq12d 6313 . . . . . . . . . . . . . 14
105104reseq2d 5279 . . . . . . . . . . . . 13
106104oveq1d 6310 . . . . . . . . . . . . 13
107105, 106eleq12d 2549 . . . . . . . . . . . 12
108101, 107imbi12d 320 . . . . . . . . . . 11 ..^ ..^
109 fourierdlem112.fcn . . . . . . . . . . 11 ..^
110108, 109chvarv 1983 . . . . . . . . . 10 ..^
111110adantlr 714 . . . . . . . . 9 ..^ ..^
11263adantr 465 . . . . . . . . 9 ..^
11363rexrd 9655 . . . . . . . . . . 11
114 pnfxr 11333 . . . . . . . . . . . 12
115114a1i 11 . . . . . . . . . . 11
11664ltpnfd 31380 . . . . . . . . . . 11
117113, 115, 64, 72, 116eliood 31418 . . . . . . . . . 10
118117adantr 465 . . . . . . . . 9 ..^
119 id 22 . . . . . . . . . . 11 ..^ ..^
12078oveq2i 6306 . . . . . . . . . . 11 ..^ ..^
121119, 120syl6eleq 2565 . . . . . . . . . 10 ..^ ..^
122121adantl 466 . . . . . . . . 9 ..^ ..^
12378oveq2i 6306 . . . . . . . . . . . 12
124 isoeq4 6217 . . . . . . . . . . . 12
125123, 124ax-mp 5 . . . . . . . . . . 11
126125iotabii 5579 . . . . . . . . . 10
12779, 126eqtri 2496 . . . . . . . . 9
12885, 95, 57, 96, 97, 99, 111, 112, 118, 122, 127fourierdlem98 31828 . . . . . . . 8 ..^
129 fourierdlem112.fbd . . . . . . . . . 10
130129adantr 465 . . . . . . . . 9 ..^
131 nfra1 2848 . . . . . . . . . . . 12
132 simpl 457 . . . . . . . . . . . . . 14
133 elioore 11571 . . . . . . . . . . . . . . 15
134133adantl 466 . . . . . . . . . . . . . 14
135 rspa 2834 . . . . . . . . . . . . . 14
136132, 134, 135syl2anc 661 . . . . . . . . . . . . 13
137136ex 434 . . . . . . . . . . . 12
138131, 137ralrimi 2867 . . . . . . . . . . 11
139138reximi 2935 . . . . . . . . . 10
140139a1i 11 . . . . . . . . 9 ..^
141130, 140mpd 15 . . . . . . . 8 ..^
142 ssid 3528 . . . . . . . . . . . . 13
143142a1i 11 . . . . . . . . . . . 12
144 dvfre 22222 . . . . . . . . . . . 12
14545, 143, 144syl2anc 661 . . . . . . . . . . 11
146145adantr 465 . . . . . . . . . 10 ..^
147 eqid 2467 . . . . . . . . . . . . . 14
14849a1i 11 . . . . . . . . . . . . . 14 ..^
14967a1i 11 . . . . . . . . . . . . . 14 ..^
150104reseq2d 5279 . . . . . . . . . . . . . . . . . 18
151150, 106eleq12d 2549 . . . . . . . . . . . . . . . . 17
152101, 151imbi12d 320 . . . . . . . . . . . . . . . 16 ..^ ..^
153 fourierdlem112.fdvcn . . . . . . . . . . . . . . . 16 ..^
154152, 153chvarv 1983 . . . . . . . . . . . . . . 15 ..^
155154adantlr 714 . . . . . . . . . . . . . 14 ..^ ..^
156 fourierdlem112.x . . . . . . . . . . . . . . . 16
15762, 156readdcld 9635 . . . . . . . . . . . . . . 15
158157adantr 465 . . . . . . . . . . . . . 14 ..^
159157rexrd 9655 . . . . . . . . . . . . . . . 16
16061, 156readdcld 9635 . . . . . . . . . . . . . . . 16
16162, 61, 156, 71ltadd1dd 10175 . . . . . . . . . . . . . . . 16
162160ltpnfd 31380 . . . . . . . . . . . . . . . 16
163159, 115, 160, 161, 162eliood 31418 . . . . . . . . . . . . . . 15
164163adantr 465 . . . . . . . . . . . . . 14 ..^
165 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . 24
166165oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . 23
167166eleq1d 2536 . . . . . . . . . . . . . . . . . . . . . 22
168167cbvrexv 3094 . . . . . . . . . . . . . . . . . . . . 21
169168rgenw 2828 . . . . . . . . . . . . . . . . . . . 20
170 rabbi 3045 . . . . . . . . . . . . . . . . . . . 20
171169, 170mpbi 208 . . . . . . . . . . . . . . . . . . 19
172171uneq2i 3660 . . . . . . . . . . . . . . . . . 18
173 isoeq5 6218 . . . . . . . . . . . . . . . . . 18
174172, 173ax-mp 5 . . . . . . . . . . . . . . . . 17
175174ax-gen 1601 . . . . . . . . . . . . . . . 16
176 iotabi 5566 . . . . . . . . . . . . . . . 16
177175, 176ax-mp 5 . . . . . . . . . . . . . . 15
178127, 177eqtri 2496 . . . . . . . . . . . . . 14
179 eleq1 2539 . . . . . . . . . . . . . . . 16
180 fveq2 5872 . . . . . . . . . . . . . . . 16
181 eqidd 2468 . . . . . . . . . . . . . . . 16
182179, 180, 181ifeq123d 31337 . . . . . . . . . . . . . . 15
183182cbvmptv 4544 . . . . . . . . . . . . . 14
18485, 147, 95, 148, 149, 57, 96, 97, 99, 155, 158, 164, 122, 178, 183fourierdlem97 31827 . . . . . . . . . . . . 13 ..^
185 cncff 21265 . . . . . . . . . . . . 13
186184, 185syl 16 . . . . . . . . . . . 12 ..^
187 fdm 5741 . . . . . . . . . . . 12
188186, 187syl 16 . . . . . . . . . . 11 ..^
189 ssdmres 5301 . . . . . . . . . . 11
190188, 189sylibr 212 . . . . . . . . . 10 ..^
191 fssres 5757 . . . . . . . . . 10
192146, 190, 191syl2anc 661 . . . . . . . . 9 ..^
19348a1i 11 . . . . . . . . . 10 ..^
194 cncffvrn 21270 . . . . . . . . . 10
195193, 184, 194syl2anc 661 . . . . . . . . 9 ..^
196192, 195mpbird 232 . . . . . . . 8 ..^
197 fourierdlem112.fdvbd . . . . . . . . . . 11
198197adantr 465 . . . . . . . . . 10 ..^
199 nfv 1683 . . . . . . . . . . . . . 14 ..^
200 nfra1 2848 . . . . . . . . . . . . . 14
201199, 200nfan 1875 . . . . . . . . . . . . 13 ..^
202 simpr 461 . . . . . . . . . . . . . . . . . 18 ..^
203 fvres 5886 . . . . . . . . . . . . . . . . . 18
204202, 203syl 16 . . . . . . . . . . . . . . . . 17 ..^
205204fveq2d 5876 . . . . . . . . . . . . . . . 16 ..^
206205adantlr 714 . . . . . . . . . . . . . . 15 ..^
207 simplr 754 . . . . . . . . . . . . . . . 16 ..^
208190sselda 3509 . . . . . . . . . . . . . . . . 17 ..^
209208adantlr 714 . . . . . . . . . . . . . . . 16 ..^
210 rspa 2834 . . . . . . . . . . . . . . . 16
211207, 209, 210syl2anc 661 . . . . . . . . . . . . . . 15 ..^
212206, 211eqbrtrd 4473 . . . . . . . . . . . . . 14 ..^
213212ex 434 . . . . . . . . . . . . 13 ..^
214201, 213ralrimi 2867 . . . . . . . . . . . 12 ..^
215214ex 434 . . . . . . . . . . 11 ..^
216215reximdv 2941 . . . . . . . . . 10 ..^
217198, 216mpd 15 . . . . . . . . 9 ..^
218 nfra1 2848 . . . . . . . . . . . 12
219203eqcomd 2475 . . . . . . . . . . . . . . . 16
220219fveq2d 5876 . . . . . . . . . . . . . . 15
221220adantl 466 . . . . . . . . . . . . . 14
222 rspa 2834 . . . . . . . . . . . . . 14
223221, 222eqbrtrd 4473 . . . . . . . . . . . . 13
224223ex 434 . . . . . . . . . . . 12
225218, 224ralrimi 2867 . . . . . . . . . . 11
226225a1i 11 . . . . . . . . . 10 ..^
227226reximdv 2941 . . . . . . . . 9 ..^
228217, 227mpd 15 . . . . . . . 8 ..^
229 nfv 1683 . . . . . . . . . . . 12 ..^
230 nfcv 2629 . . . . . . . . . . . . . 14
231230nfcsb1 3455 . . . . . . . . . . . . 13
232 nfcv 2629 . . . . . . . . . . . . 13 lim
233231, 232nfel 2642 . . . . . . . . . . . 12 lim
234229, 233nfim 1867 . . . . . . . . . . 11 ..^ lim
235 csbeq1a 3449 . . . . . . . . . . . . 13
236105, 102oveq12d 6313 . . . . . . . . . . . . 13 lim lim
237235, 236eleq12d 2549 . . . . . . . . . . . 12 lim lim
238101, 237imbi12d 320 . . . . . . . . . . 11 ..^ lim ..^ lim
239 fourierdlem112.c . . . . . . . . . . 11 ..^ lim
240234, 238, 239chvar 1982 . . . . . . . . . 10 ..^ lim
241240adantlr 714 . . . . . . . . 9 ..^ ..^ lim
24285, 95, 57, 96, 97, 99, 111, 241, 112, 118, 122, 127fourierdlem96 31826 . . . . . . . 8 ..^ ..^ ..^ ..^ lim
243230nfcsb1 3455 . . . . . . . . . . . . 13
244 nfcv 2629 . . . . . . . . . . . . 13 lim
245243, 244nfel 2642 . . . . . . . . . . . 12 lim
246229, 245nfim 1867 . . . . . . . . . . 11 ..^ lim
247 csbeq1a 3449 . . . . . . . . . . . . 13
248105, 103oveq12d 6313 . . . . . . . . . . . . 13 lim lim
249247, 248eleq12d 2549 . . . . . . . . . . . 12 lim lim
250101, 249imbi12d 320 . . . . . . . . . . 11 ..^ lim ..^ lim
251 fourierdlem112.u . . . . . . . . . . 11 ..^ lim
252246, 250, 251chvar 1982 . . . . . . . . . 10 ..^ lim
253252adantlr 714 . . . . . . . . 9 ..^ ..^ lim
25485, 95, 57, 96, 97, 99, 111, 253, 158, 164, 122, 127fourierdlem99 31829 . . . . . . . 8 ..^ ..^ ..^ ..^ lim
255 eqeq1 2471 . . . . . . . . . 10
256 eqidd 2468 . . . . . . . . . 10
257 oveq2 6303 . . . . . . . . . . . . 13
258257fveq2d 5876 . . . . . . . . . . . 12
259 breq2 4457 . . . . . . . . . . . . 13
260 eqidd 2468 . . . . . . . . . . . . 13
261 eqidd 2468 . . . . . . . . . . . . 13
262259, 260, 261ifeq123d 31337 . . . . . . . . . . . 12
263258, 262oveq12d 6313 . . . . . . . . . . 11
264 id 22 . . . . . . . . . . 11
265263, 264oveq12d 6313 . . . . . . . . . 10
266255, 256, 265ifeq123d 31337 . . . . . . . . 9
267266cbvmptv 4544 . . . . . . . 8
268 eqeq1 2471 . . . . . . . . . 10
269 eqidd 2468 . . . . . . . . . 10
270 id 22 . . . . . . . . . . 11
271 oveq1 6302 . . . . . . . . . . . . 13
272271fveq2d 5876 . . . . . . . . . . . 12
273272oveq2d 6311 . . . . . . . . . . 11
274270, 273oveq12d 6313 . . . . . . . . . 10
275268, 269, 274ifeq123d 31337 . . . . . . . . 9
276275cbvmptv 4544 . . . . . . . 8
277 fveq2 5872 . . . . . . . . . 10
278 fveq2 5872 . . . . . . . . . 10
279277, 278oveq12d 6313 . . . . . . . . 9