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

Theorem fourierdlem111 31841
 Description: The fourier partial sum for is the sum of two integrals, with the same integrand involving and the Dirichlet Kernel , but on two opposite intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem111.a
fourierdlem111.b
fourierdlem111.s
fourierdlem111.d
fourierdlem111.p ..^
fourierdlem111.m
fourierdlem111.q
fourierdlem111.x
fourierdlem111.6
fourierdlem111.fper
fourierdlem111.g
fourierdlem111.fcn ..^
fourierdlem111.r ..^ lim
fourierdlem111.l ..^ lim
fourierdlem111.t
fourierdlem111.o ..^
fourierdlem111.14
Assertion
Ref Expression
fourierdlem111
Distinct variable groups:   ,,   ,   ,,,   ,,,,   ,,,,   ,,,,,   ,,   ,,,   ,,   ,   ,,,   ,,,   ,   ,,   ,,,   ,   ,,   ,   ,,   ,,,   ,,,   ,,,,   ,   ,,   ,   ,,,,   ,,   ,
Allowed substitution hints:   ()   (,,,,,)   (,,,,,,)   (,)   (,,,,,,,)   (,)   (,,,,)   (,,,,,,,)   (,,,,,)   (,)   (,,,,)   (,,,,)   ()   (,,,,,,,)   (,)

Proof of Theorem fourierdlem111
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq1 2539 . . . . . 6
21anbi2d 703 . . . . 5
3 fveq2 5872 . . . . . 6
4 fveq2 5872 . . . . . . . . . 10
54fveq1d 5874 . . . . . . . . 9
65oveq2d 6311 . . . . . . . 8
76adantr 465 . . . . . . 7
87itgeq2dv 22056 . . . . . 6
93, 8eqeq12d 2489 . . . . 5
102, 9imbi12d 320 . . . 4
11 fourierdlem111.6 . . . . . 6
1211adantr 465 . . . . 5
13 eqid 2467 . . . . 5
14 elioore 11571 . . . . . . . . . 10
1514ssriv 3513 . . . . . . . . 9
1615a1i 11 . . . . . . . 8
1711, 16feqresmpt 5928 . . . . . . 7
18 ioossicc 11622 . . . . . . . . 9
1918a1i 11 . . . . . . . 8
20 ioombl 21843 . . . . . . . . 9
2120a1i 11 . . . . . . . 8
2211adantr 465 . . . . . . . . 9
23 pire 22718 . . . . . . . . . . . . . . . . 17
2423renegcli 9892 . . . . . . . . . . . . . . . 16
2524, 23pm3.2i 455 . . . . . . . . . . . . . . 15
26 elicc2 11601 . . . . . . . . . . . . . . 15
2725, 26ax-mp 5 . . . . . . . . . . . . . 14
2827biimpi 194 . . . . . . . . . . . . 13
2928simp1d 1008 . . . . . . . . . . . 12
3029ssriv 3513 . . . . . . . . . . 11
3130a1i 11 . . . . . . . . . 10
3231sselda 3509 . . . . . . . . 9
3322, 32ffvelrnd 6033 . . . . . . . 8
3411, 31feqresmpt 5928 . . . . . . . . . 10
3534eqcomd 2475 . . . . . . . . 9
36 fourierdlem111.p . . . . . . . . . 10 ..^
37 fourierdlem111.m . . . . . . . . . 10
38 fourierdlem111.q . . . . . . . . . 10
39 ax-resscn 9561 . . . . . . . . . . . . 13
4039a1i 11 . . . . . . . . . . . 12
4111, 40fssd 5746 . . . . . . . . . . 11
42 fssres 5757 . . . . . . . . . . 11
4341, 31, 42syl2anc 661 . . . . . . . . . 10
44 ioossicc 11622 . . . . . . . . . . . . 13
4524rexri 9658 . . . . . . . . . . . . . . 15
4645a1i 11 . . . . . . . . . . . . . 14 ..^
4723rexri 9658 . . . . . . . . . . . . . . 15
4847a1i 11 . . . . . . . . . . . . . 14 ..^
4936, 37, 38fourierdlem15 31745 . . . . . . . . . . . . . . 15
5049adantr 465 . . . . . . . . . . . . . 14 ..^
51 simpr 461 . . . . . . . . . . . . . 14 ..^ ..^
5246, 48, 50, 51fourierdlem8 31738 . . . . . . . . . . . . 13 ..^
5344, 52syl5ss 3520 . . . . . . . . . . . 12 ..^
54 resabs1 5308 . . . . . . . . . . . 12
5553, 54syl 16 . . . . . . . . . . 11 ..^
56 fourierdlem111.fcn . . . . . . . . . . 11 ..^
5755, 56eqeltrd 2555 . . . . . . . . . 10 ..^
58 fourierdlem111.r . . . . . . . . . . 11 ..^ lim
5955oveq1d 6310 . . . . . . . . . . . 12 ..^ lim lim
6059eleq2d 2537 . . . . . . . . . . 11 ..^ lim lim
6158, 60mpbird 232 . . . . . . . . . 10 ..^ lim
62 fourierdlem111.l . . . . . . . . . . 11 ..^ lim
6355oveq1d 6310 . . . . . . . . . . . 12 ..^ lim lim
6463eleq2d 2537 . . . . . . . . . . 11 ..^ lim lim
6562, 64mpbird 232 . . . . . . . . . 10 ..^ lim
6636, 37, 38, 43, 57, 61, 65fourierdlem69 31799 . . . . . . . . 9
6735, 66eqeltrd 2555 . . . . . . . 8
6819, 21, 33, 67iblss 22079 . . . . . . 7
6917, 68eqeltrd 2555 . . . . . 6
7069adantr 465 . . . . 5
71 fourierdlem111.a . . . . 5
72 fourierdlem111.b . . . . 5
73 fourierdlem111.x . . . . . 6
7473adantr 465 . . . . 5
75 fourierdlem111.s . . . . 5
76 fourierdlem111.d . . . . 5
77 simpr 461 . . . . 5
7812, 13, 70, 71, 72, 74, 75, 76, 77fourierdlem83 31813 . . . 4
7910, 78chvarv 1983 . . 3
8024a1i 11 . . . . 5
8123a1i 11 . . . . 5
8241adantr 465 . . . . . . . 8
8329adantl 466 . . . . . . . 8
84 ffvelrn 6030 . . . . . . . 8
8582, 83, 84syl2anc 661 . . . . . . 7
8685adantlr 714 . . . . . 6
8776dirkerf 31720 . . . . . . . . . 10
8887adantl 466 . . . . . . . . 9
8988adantr 465 . . . . . . . 8
9073adantr 465 . . . . . . . . . 10
9183, 90resubcld 9999 . . . . . . . . 9
9291adantlr 714 . . . . . . . 8
93 ffvelrn 6030 . . . . . . . 8
9489, 92, 93syl2anc 661 . . . . . . 7
9539, 94sseldi 3507 . . . . . 6
9686, 95mulcld 9628 . . . . 5
9780, 81, 96itgioo 22090 . . . 4
98 fvres 5886 . . . . . . . 8
9998eqcomd 2475 . . . . . . 7
10099oveq1d 6310 . . . . . 6
101100adantl 466 . . . . 5
102101itgeq2dv 22056 . . . 4
103 nfcv 2629 . . . . . . . 8
104 nfcv 2629 . . . . . . . 8
105 simpl 457 . . . . . . . . . . . . 13
106105oveq2d 6311 . . . . . . . . . . . 12
107106oveq1d 6310 . . . . . . . . . . 11
108107oveq1d 6310 . . . . . . . . . 10
109105oveq1d 6310 . . . . . . . . . . . . 13
110109oveq1d 6310 . . . . . . . . . . . 12
111110fveq2d 5876 . . . . . . . . . . 11
112111oveq1d 6310 . . . . . . . . . 10
113108, 112ifeq12d 3965 . . . . . . . . 9
114113mpteq2dva 4539 . . . . . . . 8
115103, 104, 114cbvmpt 4543 . . . . . . 7
11676, 115eqtri 2496 . . . . . 6
117 nfcv 2629 . . . . . . 7
118 nfcv 2629 . . . . . . 7
119 fveq2 5872 . . . . . . . 8
120 oveq1 6302 . . . . . . . . 9
121120fveq2d 5876 . . . . . . . 8
122119, 121oveq12d 6313 . . . . . . 7
123117, 118, 122cbvmpt 4543 . . . . . 6
12438adantr 465 . . . . . 6
12537adantr 465 . . . . . 6
126 simpr 461 . . . . . 6
12773adantr 465 . . . . . 6
12843adantr 465 . . . . . 6
12957adantlr 714 . . . . . 6 ..^
13061adantlr 714 . . . . . 6 ..^ lim
13165adantlr 714 . . . . . 6 ..^ lim
132116, 36, 123, 124, 125, 126, 127, 128, 129, 130, 131fourierdlem101 31831 . . . . 5
133 oveq2 6303 . . . . . . . . . 10
134133fveq2d 5876 . . . . . . . . 9
135 fveq2 5872 . . . . . . . . 9
136134, 135oveq12d 6313 . . . . . . . 8
137 nfcv 2629 . . . . . . . 8
138 nfcv 2629 . . . . . . . 8
139136, 137, 138cbvitg 22050 . . . . . . 7
140139a1i 11 . . . . . 6
14124a1i 11 . . . . . . . . . . 11
142141, 73jca 532 . . . . . . . . . 10
143 resubcl 9895 . . . . . . . . . 10
144142, 143syl 16 . . . . . . . . 9
145144adantr 465 . . . . . . . 8
14623a1i 11 . . . . . . . . . . 11
147146, 73jca 532 . . . . . . . . . 10
148 resubcl 9895 . . . . . . . . . 10
149147, 148syl 16 . . . . . . . . 9
150149adantr 465 . . . . . . . 8
15141adantr 465 . . . . . . . . . . 11
15273adantr 465 . . . . . . . . . . . 12
153 simpr 461 . . . . . . . . . . . . . 14
154144adantr 465 . . . . . . . . . . . . . . 15
155149adantr 465 . . . . . . . . . . . . . . 15
156 elicc2 11601 . . . . . . . . . . . . . . 15
157154, 155, 156syl2anc 661 . . . . . . . . . . . . . 14
158153, 157mpbid 210 . . . . . . . . . . . . 13
159158simp1d 1008 . . . . . . . . . . . 12
160152, 159readdcld 9635 . . . . . . . . . . 11
161 ffvelrn 6030 . . . . . . . . . . 11
162151, 160, 161syl2anc 661 . . . . . . . . . 10
163162adantlr 714 . . . . . . . . 9
16488adantr 465 . . . . . . . . . . 11
165159adantlr 714 . . . . . . . . . . 11
166 ffvelrn 6030 . . . . . . . . . . 11
167164, 165, 166syl2anc 661 . . . . . . . . . 10
16839, 167sseldi 3507 . . . . . . . . 9
169163, 168mulcld 9628 . . . . . . . 8
170145, 150, 169itgioo 22090 . . . . . . 7
17139, 73sseldi 3507 . . . . . . . . . . . . . . . . . 18
17239, 146sseldi 3507 . . . . . . . . . . . . . . . . . . 19
173172negcld 9929 . . . . . . . . . . . . . . . . . 18
174171, 173pncan3d 9945 . . . . . . . . . . . . . . . . 17
175174eqcomd 2475 . . . . . . . . . . . . . . . 16
176175adantr 465 . . . . . . . . . . . . . . 15
177158simp2d 1009 . . . . . . . . . . . . . . . 16
178154, 159, 152, 177leadd2dd 10179 . . . . . . . . . . . . . . 15
179176, 178eqbrtrd 4473 . . . . . . . . . . . . . 14
180158simp3d 1010 . . . . . . . . . . . . . . . 16
181159, 155, 152, 180leadd2dd 10179 . . . . . . . . . . . . . . 15
182171adantr 465 . . . . . . . . . . . . . . . 16
183172adantr 465 . . . . . . . . . . . . . . . 16
184182, 183pncan3d 9945 . . . . . . . . . . . . . . 15
185181, 184breqtrd 4477 . . . . . . . . . . . . . 14
186160, 179, 1853jca 1176 . . . . . . . . . . . . 13
18724a1i 11 . . . . . . . . . . . . . 14
18823a1i 11 . . . . . . . . . . . . . 14
189 elicc2 11601 . . . . . . . . . . . . . 14
190187, 188, 189syl2anc 661 . . . . . . . . . . . . 13
191186, 190mpbird 232 . . . . . . . . . . . 12
192 fvres 5886 . . . . . . . . . . . 12
193191, 192syl 16 . . . . . . . . . . 11
194193eqcomd 2475 . . . . . . . . . 10
195194adantlr 714 . . . . . . . . 9
196195oveq1d 6310 . . . . . . . 8
197196itgeq2dv 22056 . . . . . . 7
198170, 197eqtrd 2508 . . . . . 6
199140, 198eqtr2d 2509 . . . . 5
200132, 199eqtrd 2508 . . . 4
20197, 102, 2003eqtrd 2512 . . 3
202 elioore 11571 . . . . . . . . 9
203202adantl 466 . . . . . . . 8
20441adantr 465 . . . . . . . . . . 11
20573adantr 465 . . . . . . . . . . . 12
206202adantl 466 . . . . . . . . . . . 12
207205, 206readdcld 9635 . . . . . . . . . . 11
208204, 207ffvelrnd 6033 . . . . . . . . . 10
209208adantlr 714 . . . . . . . . 9
21039a1i 11 . . . . . . . . . 10
21188adantr 465 . . . . . . . . . . 11
212211, 203ffvelrnd 6033 . . . . . . . . . 10
213210, 212sseldd 3510 . . . . . . . . 9
214209, 213mulcld 9628 . . . . . . . 8
215 fourierdlem111.g . . . . . . . . . 10
216 oveq2 6303 . . . . . . . . . . . . 13
217216fveq2d 5876 . . . . . . . . . . . 12
218 fveq2 5872 . . . . . . . . . . . 12
219217, 218oveq12d 6313 . . . . . . . . . . 11
220219cbvmptv 4544 . . . . . . . . . 10
221215, 220eqtri 2496 . . . . . . . . 9
222221fvmpt2 5964 . . . . . . . 8
223203, 214, 222syl2anc 661 . . . . . . 7
224223eqcomd 2475 . . . . . 6
225224itgeq2dv 22056 . . . . 5
226 eqidd 2468 . . . . 5
22741adantr 465 . . . . . . . . . . . . 13
22873adantr 465 . . . . . . . . . . . . . 14
229 simpr 461 . . . . . . . . . . . . . 14
230228, 229readdcld 9635 . . . . . . . . . . . . 13
231227, 230ffvelrnd 6033 . . . . . . . . . . . 12
232231adantlr 714 . . . . . . . . . . 11
23339a1i 11 . . . . . . . . . . . 12
23488ffvelrnda 6032 . . . . . . . . . . . 12
235233, 234sseldd 3510 . . . . . . . . . . 11
236232, 235mulcld 9628 . . . . . . . . . 10
237236, 215fmptd 6056 . . . . . . . . 9
238237adantr 465 . . . . . . . 8
239144adantr 465 . . . . . . . . . 10
240149adantr 465 . . . . . . . . . 10
241 simpr 461 . . . . . . . . . 10
242 eliccre 31427 . . . . . . . . . 10
243239, 240, 241, 242syl3anc 1228 . . . . . . . . 9
244243adantlr 714 . . . . . . . 8
245238, 244ffvelrnd 6033 . . . . . . 7
246145, 150, 245itgioo 22090 . . . . . 6
247 fveq2 5872 . . . . . . . 8
248247cbvitgv 22051 . . . . . . 7
249248a1i 11 . . . . . 6
250246, 249eqtrd 2508 . . . . 5
251225, 226, 2503eqtrd 2512 . . . 4
252 eqid 2467 . . . . . . 7
253127renegcld 9998 . . . . . . 7
254 fourierdlem111.o . . . . . . 7 ..^
25536fourierdlem2 31732 . . . . . . . . . . . . . . . . . . . 20 ..^
25637, 255syl 16 . . . . . . . . . . . . . . . . . . 19 ..^
25738, 256mpbid 210 . . . . . . . . . . . . . . . . . 18 ..^
258257simpld 459 . . . . . . . . . . . . . . . . 17
259 elmapi 7452 . . . . . . . . . . . . . . . . 17
260258, 259syl 16 . . . . . . . . . . . . . . . 16
261260adantr 465 . . . . . . . . . . . . . . 15
262 simpr 461 . . . . . . . . . . . . . . 15
263261, 262ffvelrnd 6033 . . . . . . . . . . . . . 14
26473adantr 465 . . . . . . . . . . . . . 14
265263, 264resubcld 9999 . . . . . . . . . . . . 13
266265ralrimiva 2881 . . . . . . . . . . . 12
267 fourierdlem111.14 . . . . . . . . . . . . 13
268267fmpt 6053 . . . . . . . . . . . 12
269266, 268sylib 196 . . . . . . . . . . 11
270 reex 9595 . . . . . . . . . . . . . 14
271 ovex 6320 . . . . . . . . . . . . . 14
272270, 271pm3.2i 455 . . . . . . . . . . . . 13
273272a1i 11 . . . . . . . . . . . 12
274 elmapg 7445 . . . . . . . . . . . 12
275273, 274syl 16 . . . . . . . . . . 11
276269, 275mpbird 232 . . . . . . . . . 10
277267a1i 11 . . . . . . . . . . . . 13
278 fveq2 5872 . . . . . . . . . . . . . . . 16
279278adantl 466 . . . . . . . . . . . . . . 15
280257simprd 463 . . . . . . . . . . . . . . . . . 18 ..^
281280simpld 459 . . . . . . . . . . . . . . . . 17
282281simpld 459 . . . . . . . . . . . . . . . 16
283282adantr 465 . . . . . . . . . . . . . . 15
284 eqidd 2468 . . . . . . . . . . . . . . 15
285279, 283, 2843eqtrd 2512 . . . . . . . . . . . . . 14
286285oveq1d 6310 . . . . . . . . . . . . 13
287 0z 10887 . . . . . . . . . . . . . . . . 17
288287a1i 11 . . . . . . . . . . . . . . . 16
28937nnzd 10977 . . . . . . . . . . . . . . . 16
290 0re 9608 . . . . . . . . . . . . . . . . . . 19
291290a1i 11 . . . . . . . . . . . . . . . . . 18
292 nnre 10555 . . . . . . . . . . . . . . . . . 18
293 nngt0 10577 . . . . . . . . . . . . . . . . . 18
294291, 292, 293ltled 9744 . . . . . . . . . . . . . . . . 17
29537, 294syl 16 . . . . . . . . . . . . . . . 16
296288, 289, 2953jca 1176 . . . . . . . . . . . . . . 15
297 eluz2 11100 . . . . . . . . . . . . . . 15
298296, 297sylibr 212 . . . . . . . . . . . . . 14
299 eluzfz1 11705 . . . . . . . . . . . . . 14
300298, 299syl 16 . . . . . . . . . . . . 13
301277, 286, 300, 144fvmptd 5962 . . . . . . . . . . . 12
302 fveq2 5872 . . . . . . . . . . . . . . . 16
303302adantl 466 . . . . . . . . . . . . . . 15
304281simprd 463 . . . . . . . . . . . . . . . 16
305304adantr 465 . . . . . . . . . . . . . . 15
306303, 305eqtrd 2508 . . . . . . . . . . . . . 14
307306oveq1d 6310 . . . . . . . . . . . . 13
308 eluzfz2 11706 . . . . . . . . . . . . . 14
309298, 308syl 16 . . . . . . . . . . . . 13
310277, 307, 309, 149fvmptd 5962 . . . . . . . . . . . 12
311301, 310jca 532 . . . . . . . . . . 11
312280simprd 463 . . . . . . . . . . . . . . 15 ..^
313312r19.21bi 2836 . . . . . . . . . . . . . 14 ..^
314260adantr 465 . . . . . . . . . . . . . . . 16 ..^
315 elfzofz 11823 . . . . . . . . . . . . . . . . 17 ..^
316315adantl 466 . . . . . . . . . . . . . . . 16 ..^
317314, 316ffvelrnd 6033 . . . . . . . . . . . . . . 15 ..^
318 fzofzp1 11889 . . . . . . . . . . . . . . . . 17 ..^
319318adantl 466 . . . . . . . . . . . . . . . 16 ..^
320314, 319ffvelrnd 6033 . . . . . . . . . . . . . . 15 ..^
32173adantr 465 . . . . . . . . . . . . . . 15 ..^
322317, 320, 321ltsub1d 10173 . . . . . . . . . . . . . 14 ..^
323313, 322mpbid 210 . . . . . . . . . . . . 13 ..^
324316, 265syldan 470 . . . . . . . . . . . . . . 15 ..^
325267fvmpt2 5964 . . . . . . . . . . . . . . 15
326316, 324, 325syl2anc 661 . . . . . . . . . . . . . 14 ..^
327 fveq2 5872 . . . . . . . . . . . . . . . . . . 19
328327oveq1d 6310 . . . . . . . . . . . . . . . . . 18
329328cbvmptv 4544 . . . . . . . . . . . . . . . . 17
330267, 329eqtri 2496 . . . . . . . . . . . . . . . 16
331330a1i 11 . . . . . . . . . . . . . . 15 ..^
332 fveq2 5872 . . . . . . . . . . . . . . . . 17
333332oveq1d 6310 . . . . . . . . . . . . . . . 16
334333adantl 466 . . . . . . . . . . . . . . 15 ..^
335320, 321resubcld 9999 . . . . . . . . . . . . . . 15 ..^
336331, 334, 319, 335fvmptd 5962 . . . . . . . . . . . . . 14 ..^
337326, 336breq12d 4466 . . . . . . . . . . . . 13 ..^
338323, 337mpbird 232 . . . . . . . . . . . 12 ..^
339338ralrimiva 2881 . . . . . . . . . . 11 ..^
340311, 339jca 532 . . . . . . . . . 10 ..^
341276, 340jca 532 . . . . . . . . 9 ..^
342254fourierdlem2 31732 . . . . . . . . . 10 ..^
34337, 342syl 16 . . . . . . . . 9 ..^
344341, 343mpbird 232 . . . . . . . 8
345344adantr 465 . . . . . . 7
346172, 173, 171nnncan2d 9977 . . . . . . . . . . . 12
34739, 23sselii 3506 . . . . . . . . . . . . . 14
348347, 347subnegi 9910 . . . . . . . . . . . . 13
349348a1i 11 . . . . . . . . . . . 12
350 fourierdlem111.t . . . . . . . . . . . . . 14
3513472timesi 10668 . . . . . . . . . . . . . . 15
352351, 348eqtr4i 2499 . . . . . . . . . . . . . 14
353350, 352eqtri 2496 . . . . . . . . . . . . 13
354353, 349syl5req 2521 . . . . . . . . . . . 12
355346, 349, 3543eqtrd 2512 . . . . . . . . . . 11
356355oveq2d 6311 . . . . . . . . . 10
357356fveq2d 5876 . . . . . . . . 9
358357ad2antrr 725 . . . . . . . 8
359 simpr 461 . . . . . . . . . 10
360215fvmpt2 5964 . . . . . . . . . 10
361359, 236, 360syl2anc 661 . . . . . . . . 9
362171adantr 465 . . . . . . . . . . . . . . 15
36339, 229sseldi 3507 . . . . . . . . . . . . . . 15
364 2re 10617 . . . . . . . . . . . . . . . . . . . 20
365364, 23remulcli 9622 . . . . . . . . . . . . . . . . . . 19
366350, 365eqeltri 2551 . . . . . . . . . . . . . . . . . 18
367366a1i 11 . . . . . . . . . . . . . . . . 17
36839, 367sseldi 3507 . . . . . . . . . . . . . . . 16
369368adantr 465 . . . . . . . . . . . . . . 15
370362, 363, 369addassd 9630 . . . . . . . . . . . . . 14
371370eqcomd 2475 . . . . . . . . . . . . 13
372371fveq2d 5876 . . . . . . . . . . . 12
373 simpl 457 . . . . . . . . . . . . . 14
374373, 230jca 532 . . . . . . . . . . . . 13
375 eleq1 2539 . . . . . . . . . . . . . . . 16
376375anbi2d 703 . . . . . . . . . . . . . . 15
377 oveq1 6302 . . . . . . . . . . . . . . . . 17
378377fveq2d 5876 . . . . . . . . . . . . . . . 16
379 fveq2 5872 . . . . . . . . . . . . . . . 16
380378, 379eqeq12d 2489 . . . . . . . . . . . . . . 15
381376, 380imbi12d 320 . . . . . . . . . . . . . 14
382 nfv 1683 . . . . . . . . . . . . . . 15
383 eleq1 2539 . . . . . . . . . . . . . . . . 17
384383anbi2d 703 . . . . . . . . . . . . . . . 16
385 oveq1 6302 . . . . . . . . . . . . . . . . . 18
386385fveq2d 5876 . . . . . . . . . . . . . . . . 17
387 fveq2 5872 . . . . . . . . . . . . . . . . 17
388386, 387eqeq12d 2489 . . . . . . . . . . . . . . . 16
389384, 388imbi12d 320 . . . . . . . . . . . . . . 15
390 fourierdlem111.fper . . . . . . . . . . . . . . 15
391382, 389, 390chvar 1982 . . . . . . . . . . . . . 14
392381, 391vtoclg 3176 . . . . . . . . . . . . 13
393230, 374, 392sylc 60 . . . . . . . . . . . 12
394372, 393eqtr2d 2509 . . . . . . . . . . 11
395394adantlr 714 . . . . . . . . . 10
39676, 350dirkerper 31719 . . . . . . . . . . . 12
397396eqcomd 2475 . . . . . . . . . . 11
398397adantll 713 . . . . . . . . . 10
399395, 398oveq12d 6313 . . . . . . . . 9
400221a1i 11 . . . . . . . . . . 11
401 oveq2 6303 . . . . . . . . . . . . . 14
402401fveq2d 5876 . . . . . . . . . . . . 13
403 fveq2 5872 . . . . . . . . . . . . 13
404402, 403oveq12d 6313 . . . . . . . . . . . 12
405404adantl 466 . . . . . . . . . . 11
406367ad2antrr 725 . . . . . . . . . . . 12
407359, 406readdcld 9635 . . . . . . . . . . 11
408367adantr 465 . . . . . . . . . . . . . . . 16
409229, 408readdcld 9635 . . . . . . . . . . . . . . 15
410228, 409readdcld 9635 . . . . . . . . . . . . . 14
411227, 410ffvelrnd 6033 . . . . . . . . . . . . 13
412411adantlr 714 . . . . . . . . . . . 12
41388adantr 465 . . . . . . . . . . . . . 14
414413, 407ffvelrnd 6033 . . . . . . . . . . . . 13
415233, 414sseldd 3510 . . . . . . . . . . . 12
416412, 415mulcld 9628 . . . . . . . . . . 11
417400, 405, 407, 416fvmptd 5962 . . . . . . . . . 10
418417eqcomd 2475 . . . . . . . . 9
419361, 399, 4183eqtrrd 2513 . . . . . . . 8
420358, 419eqtrd 2508 . . . . . . 7
421221reseq1i 5275 . . . . . . . . . 10
422421a1i 11 . . . . . . . . 9 ..^
423 ioossre 11598 . . . . . . . . . . 11
424 resmpt 5329 . . . . . . . . . . 11
425423, 424ax-mp 5 . . . . . . . . . 10
426425a1i 11 <