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

Theorem fourierdlem81 31811
 Description: The integral of a piecewise continuous periodic function is unchanged if the domain is shifted by its period . In this lemma, is assumed to be strictly positive. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem81.a
fourierdlem81.b
fourierdlem81.p ..^
fourierdlem81.m
fourierdlem81.t
fourierdlem81.q
fourierdlem81.fper
fourierdlem81.s
fourierdlem81.f
fourierdlem81.cncf ..^
fourierdlem81.r ..^ lim
fourierdlem81.l ..^ lim
fourierdlem81.g
fourierdlem81.h
Assertion
Ref Expression
fourierdlem81
Distinct variable groups:   ,,,   ,,   ,,,   ,   ,,   ,   ,   ,,,   ,   ,,   ,   ,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,,,)   ()   (,,)   (,)   (,)   (,)   (,,)   (,,,)   (,,)

Proof of Theorem fourierdlem81
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem81.q . . . . . . . . 9
2 fourierdlem81.m . . . . . . . . . 10
3 fourierdlem81.p . . . . . . . . . . 11 ..^
43fourierdlem2 31732 . . . . . . . . . 10 ..^
52, 4syl 16 . . . . . . . . 9 ..^
61, 5mpbid 210 . . . . . . . 8 ..^
76simprd 463 . . . . . . 7 ..^
87simpld 459 . . . . . 6
98simpld 459 . . . . 5
109eqcomd 2475 . . . 4
118simprd 463 . . . . 5
1211eqcomd 2475 . . . 4
1310, 12oveq12d 6313 . . 3
14 itgeq1 22047 . . 3
1513, 14syl 16 . 2
16 0z 10887 . . . 4
1716a1i 11 . . 3
18 0p1e1 10659 . . . . . . 7
1918fveq2i 5875 . . . . . 6
20 nnuz 11129 . . . . . . 7
2120eqcomi 2480 . . . . . 6
2219, 21eqtr2i 2497 . . . . 5
2322a1i 11 . . . 4
242, 23eleqtrd 2557 . . 3
256simpld 459 . . . 4
26 reex 9595 . . . . . 6
2726a1i 11 . . . . 5
28 ovex 6320 . . . . . 6
2928a1i 11 . . . . 5
30 elmapg 7445 . . . . 5
3127, 29, 30syl2anc 661 . . . 4
3225, 31mpbid 210 . . 3
337simprd 463 . . . 4 ..^
3433r19.21bi 2836 . . 3 ..^
35 fourierdlem81.f . . . . 5
3635adantr 465 . . . 4
37 fourierdlem81.a . . . . . . . 8
389, 37eqeltrd 2555 . . . . . . 7
39 fourierdlem81.b . . . . . . . 8
4011, 39eqeltrd 2555 . . . . . . 7
41 iccssre 11618 . . . . . . 7
4238, 40, 41syl2anc 661 . . . . . 6
4342adantr 465 . . . . 5
44 simpr 461 . . . . 5
4543, 44sseldd 3510 . . . 4
4636, 45ffvelrnd 6033 . . 3
4732adantr 465 . . . . 5 ..^
48 elfzofz 11823 . . . . . 6 ..^
4948adantl 466 . . . . 5 ..^
5047, 49ffvelrnd 6033 . . . 4 ..^
51 fzofzp1 11889 . . . . . 6 ..^
5251adantl 466 . . . . 5 ..^
5347, 52ffvelrnd 6033 . . . 4 ..^
5435feqmptd 5927 . . . . . . . 8
5554reseq1d 5278 . . . . . . 7
5655adantr 465 . . . . . 6 ..^
57 ioossre 11598 . . . . . . . 8
5857a1i 11 . . . . . . 7 ..^
59 resmpt 5329 . . . . . . 7
6058, 59syl 16 . . . . . 6 ..^
61 eqidd 2468 . . . . . 6 ..^
6256, 60, 613eqtrrd 2513 . . . . 5 ..^
63 fourierdlem81.cncf . . . . . 6 ..^
64 fourierdlem81.l . . . . . 6 ..^ lim
65 fourierdlem81.r . . . . . 6 ..^ lim
6650, 53, 63, 64, 65iblcncfioo 31619 . . . . 5 ..^
6762, 66eqeltrd 2555 . . . 4 ..^
6835ad2antrr 725 . . . . 5 ..^
69 iccssre 11618 . . . . . . 7
7050, 53, 69syl2anc 661 . . . . . 6 ..^
7170sselda 3509 . . . . 5 ..^
7268, 71ffvelrnd 6033 . . . 4 ..^
7350, 53, 67, 72ibliooicc 31612 . . 3 ..^
7417, 24, 32, 34, 46, 73itgspltprt 31620 . 2 ..^
75 fourierdlem81.s . . . . . . . 8
7675a1i 11 . . . . . . 7
77 fveq2 5872 . . . . . . . . 9
7877oveq1d 6310 . . . . . . . 8
7978adantl 466 . . . . . . 7
802nnnn0d 10864 . . . . . . . . 9
81 nn0uz 11128 . . . . . . . . . 10
8281a1i 11 . . . . . . . . 9
8380, 82eleqtrd 2557 . . . . . . . 8
84 eluzfz1 11705 . . . . . . . 8
8583, 84syl 16 . . . . . . 7
86 fourierdlem81.t . . . . . . . . 9
8786rpred 11268 . . . . . . . 8
8838, 87readdcld 9635 . . . . . . 7
8976, 79, 85, 88fvmptd 5962 . . . . . 6
909oveq1d 6310 . . . . . 6
9189, 90eqtr2d 2509 . . . . 5
92 fveq2 5872 . . . . . . . . 9
93 eqidd 2468 . . . . . . . . 9
9492, 93oveq12d 6313 . . . . . . . 8
9594adantl 466 . . . . . . 7
96 eluzfz2 11706 . . . . . . . 8
9783, 96syl 16 . . . . . . 7
9840, 87readdcld 9635 . . . . . . 7
9976, 95, 97, 98fvmptd 5962 . . . . . 6
10011oveq1d 6310 . . . . . 6
10199, 100eqtr2d 2509 . . . . 5
10291, 101oveq12d 6313 . . . 4
103 itgeq1 22047 . . . 4
104102, 103syl 16 . . 3
10532ffvelrnda 6032 . . . . . 6
10687adantr 465 . . . . . 6
107105, 106readdcld 9635 . . . . 5
108107, 75fmptd 6056 . . . 4
10987adantr 465 . . . . . . 7 ..^
11050, 53, 109ltadd1d 10157 . . . . . 6 ..^
11134, 110mpbid 210 . . . . 5 ..^
11249, 107syldan 470 . . . . . . 7 ..^
11375fvmpt2 5964 . . . . . . 7
11449, 112, 113syl2anc 661 . . . . . 6 ..^
115 nfcv 2629 . . . . . . . . . 10
116 nfcv 2629 . . . . . . . . . 10
117 fveq2 5872 . . . . . . . . . . 11
118117oveq1d 6310 . . . . . . . . . 10
119115, 116, 118cbvmpt 4543 . . . . . . . . 9
12075, 119eqtri 2496 . . . . . . . 8
121120a1i 11 . . . . . . 7 ..^
122 fveq2 5872 . . . . . . . . 9
123122oveq1d 6310 . . . . . . . 8
124123adantl 466 . . . . . . 7 ..^
12553, 109readdcld 9635 . . . . . . 7 ..^
126121, 124, 52, 125fvmptd 5962 . . . . . 6 ..^
127114, 126breq12d 4466 . . . . 5 ..^
128111, 127mpbird 232 . . . 4 ..^
12935adantr 465 . . . . 5
13089, 88eqeltrd 2555 . . . . . . . 8
131130adantr 465 . . . . . . 7
13299, 98eqeltrd 2555 . . . . . . . 8
133132adantr 465 . . . . . . 7
134 iccssre 11618 . . . . . . 7
135131, 133, 134syl2anc 661 . . . . . 6
136 simpr 461 . . . . . 6
137135, 136sseldd 3510 . . . . 5
138129, 137ffvelrnd 6033 . . . 4
139114, 112eqeltrd 2555 . . . . 5 ..^
140126, 125eqeltrd 2555 . . . . 5 ..^
141 ioosscn 31414 . . . . . . . . 9
142141a1i 11 . . . . . . . 8 ..^
143 nfcv 2629 . . . . . . . . 9
144 nfcv 2629 . . . . . . . . 9
145 nfv 1683 . . . . . . . . 9
146 nfv 1683 . . . . . . . . 9
147 eqeq1 2471 . . . . . . . . . . 11
148147rexbidv 2978 . . . . . . . . . 10
149 nfv 1683 . . . . . . . . . . . 12
150 nfv 1683 . . . . . . . . . . . 12
151 oveq1 6302 . . . . . . . . . . . . 13
152151eqeq2d 2481 . . . . . . . . . . . 12
153149, 150, 152cbvrex 3090 . . . . . . . . . . 11
154153a1i 11 . . . . . . . . . 10
155148, 154bitrd 253 . . . . . . . . 9
156143, 144, 145, 146, 155cbvrab 3116 . . . . . . . 8
157 fdm 5741 . . . . . . . . . . . 12
15835, 157syl 16 . . . . . . . . . . 11
159 feq2 5720 . . . . . . . . . . 11
160158, 159syl 16 . . . . . . . . . 10
16135, 160mpbird 232 . . . . . . . . 9
162161adantr 465 . . . . . . . 8 ..^
16357sseli 3505 . . . . . . . . . . . . . . . . . 18
164163adantl 466 . . . . . . . . . . . . . . . . 17
16587adantr 465 . . . . . . . . . . . . . . . . 17
166164, 165readdcld 9635 . . . . . . . . . . . . . . . 16
167166adantlr 714 . . . . . . . . . . . . . . 15 ..^
1681673adant3 1016 . . . . . . . . . . . . . 14 ..^
169 simp3 998 . . . . . . . . . . . . . . 15 ..^
1701583ad2ant1 1017 . . . . . . . . . . . . . . . 16
1711703adant1r 1221 . . . . . . . . . . . . . . 15 ..^
172169, 171eleq12d 2549 . . . . . . . . . . . . . 14 ..^
173168, 172mpbird 232 . . . . . . . . . . . . 13 ..^
1741733exp 1195 . . . . . . . . . . . 12 ..^
175174adantr 465 . . . . . . . . . . 11 ..^
176175rexlimdv 2957 . . . . . . . . . 10 ..^
177176ralrimiva 2881 . . . . . . . . 9 ..^
178 rabss 3582 . . . . . . . . 9
179177, 178sylibr 212 . . . . . . . 8 ..^
180 simpl 457 . . . . . . . . . 10
181180adantlr 714 . . . . . . . . 9 ..^
18237rexrd 9655 . . . . . . . . . . 11
183181, 182syl 16 . . . . . . . . . 10 ..^
18439rexrd 9655 . . . . . . . . . . 11
185181, 184syl 16 . . . . . . . . . 10 ..^
1863, 2, 1fourierdlem15 31745 . . . . . . . . . . 11
187181, 186syl 16 . . . . . . . . . 10 ..^
188 simpr 461 . . . . . . . . . . 11 ..^ ..^
189188adantr 465 . . . . . . . . . 10 ..^ ..^
190 ioossicc 11622 . . . . . . . . . . . 12
191190sseli 3505 . . . . . . . . . . 11
192191adantl 466 . . . . . . . . . 10 ..^
193183, 185, 187, 189, 192fourierdlem1 31731 . . . . . . . . 9 ..^
194 fourierdlem81.fper . . . . . . . . 9
195181, 193, 194syl2anc 661 . . . . . . . 8 ..^
196142, 109, 156, 162, 179, 195, 63cncfperiod 31540 . . . . . . 7 ..^
197 nfv 1683 . . . . . . . . . . . 12 ..^
198 simpl 457 . . . . . . . . . . . . . . . 16 ..^ ..^
199148elrab 3266 . . . . . . . . . . . . . . . . . 18
200199simprbi 464 . . . . . . . . . . . . . . . . 17
201200adantl 466 . . . . . . . . . . . . . . . 16 ..^
202198, 201jca 532 . . . . . . . . . . . . . . 15 ..^ ..^
203 simpr 461 . . . . . . . . . . . . . . . . 17 ..^
204 nfv 1683 . . . . . . . . . . . . . . . . . . 19 ..^
205 nfre1 2928 . . . . . . . . . . . . . . . . . . 19
206204, 205nfan 1875 . . . . . . . . . . . . . . . . . 18 ..^
207 nfv 1683 . . . . . . . . . . . . . . . . . 18
208 simp3 998 . . . . . . . . . . . . . . . . . . . . . . 23
2091663adant3 1016 . . . . . . . . . . . . . . . . . . . . . . 23
210208, 209eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . 22
2112103adant1r 1221 . . . . . . . . . . . . . . . . . . . . 21 ..^
212 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
21350rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
214213adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
21553rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
216215adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
217 elioo2 11582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
218214, 216, 217syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
219212, 218mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
220219simp2d 1009 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
22150adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
222163adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
223109adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
224221, 222, 223ltadd1d 10157 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
225220, 224mpbid 210 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
2262253adant3 1016 . . . . . . . . . . . . . . . . . . . . . 22 ..^
2271143ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
228 simp3 998 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
229227, 228breq12d 4466 . . . . . . . . . . . . . . . . . . . . . 22 ..^
230226, 229mpbird 232 . . . . . . . . . . . . . . . . . . . . 21 ..^
231219simp3d 1010 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
23253adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
233222, 232, 223ltadd1d 10157 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
234231, 233mpbid 210 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
2352343adant3 1016 . . . . . . . . . . . . . . . . . . . . . 22 ..^
2361263ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
237228, 236breq12d 4466 . . . . . . . . . . . . . . . . . . . . . 22 ..^
238235, 237mpbird 232 . . . . . . . . . . . . . . . . . . . . 21 ..^
239211, 230, 2383jca 1176 . . . . . . . . . . . . . . . . . . . 20 ..^
2402393exp 1195 . . . . . . . . . . . . . . . . . . 19 ..^
241240adantr 465 . . . . . . . . . . . . . . . . . 18 ..^
242206, 207, 241rexlimd 2951 . . . . . . . . . . . . . . . . 17 ..^
243203, 242mpd 15 . . . . . . . . . . . . . . . 16 ..^
244139rexrd 9655 . . . . . . . . . . . . . . . . . 18 ..^
245244adantr 465 . . . . . . . . . . . . . . . . 17 ..^
246140rexrd 9655 . . . . . . . . . . . . . . . . . 18 ..^
247246adantr 465 . . . . . . . . . . . . . . . . 17 ..^
248 elioo2 11582 . . . . . . . . . . . . . . . . 17
249245, 247, 248syl2anc 661 . . . . . . . . . . . . . . . 16 ..^
250243, 249mpbird 232 . . . . . . . . . . . . . . 15 ..^
251202, 250syl 16 . . . . . . . . . . . . . 14 ..^
252251ex 434 . . . . . . . . . . . . 13 ..^
253 elioore 11571 . . . . . . . . . . . . . . . . . 18
254 ax-resscn 9561 . . . . . . . . . . . . . . . . . . 19
255254sseli 3505 . . . . . . . . . . . . . . . . . 18
256253, 255syl 16 . . . . . . . . . . . . . . . . 17
257256adantl 466 . . . . . . . . . . . . . . . 16 ..^
258253adantl 466 . . . . . . . . . . . . . . . . . . . . 21
25987adantr 465 . . . . . . . . . . . . . . . . . . . . 21
260258, 259resubcld 9999 . . . . . . . . . . . . . . . . . . . 20
261260adantlr 714 . . . . . . . . . . . . . . . . . . 19 ..^
262114oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . 22 ..^
263254, 50sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
264254, 109sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
265263, 264pncand 9943 . . . . . . . . . . . . . . . . . . . . . 22 ..^
266262, 265eqtr2d 2509 . . . . . . . . . . . . . . . . . . . . 21 ..^
267266adantr 465 . . . . . . . . . . . . . . . . . . . 20 ..^
268 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
269244adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
270246adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
271269, 270, 248syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
272268, 271mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22 ..^
273272simp2d 1009 . . . . . . . . . . . . . . . . . . . . 21 ..^
274139adantr 465 . . . . . . . . . . . . . . . . . . . . . 22 ..^
275253adantl 466 . . . . . . . . . . . . . . . . . . . . . 22 ..^
276109adantr 465 . . . . . . . . . . . . . . . . . . . . . 22 ..^
277274, 275, 276ltsub1d 10173 . . . . . . . . . . . . . . . . . . . . 21 ..^
278273, 277mpbid 210 . . . . . . . . . . . . . . . . . . . 20 ..^
279267, 278eqbrtrd 4473 . . . . . . . . . . . . . . . . . . 19 ..^
280272simp3d 1010 . . . . . . . . . . . . . . . . . . . . 21 ..^
281140adantr 465 . . . . . . . . . . . . . . . . . . . . . 22 ..^
282275, 281, 276ltsub1d 10173 . . . . . . . . . . . . . . . . . . . . 21 ..^
283280, 282mpbid 210 . . . . . . . . . . . . . . . . . . . 20 ..^
284126oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . 22 ..^
285254, 53sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
286285, 264pncand 9943 . . . . . . . . . . . . . . . . . . . . . 22 ..^
287284, 286eqtrd 2508 . . . . . . . . . . . . . . . . . . . . 21 ..^
288287adantr 465 . . . . . . . . . . . . . . . . . . . 20 ..^
289283, 288breqtrd 4477 . . . . . . . . . . . . . . . . . . 19 ..^
290261, 279, 2893jca 1176 . . . . . . . . . . . . . . . . . 18 ..^
291213adantr 465 . . . . . . . . . . . . . . . . . . 19 ..^
292215adantr 465 . . . . . . . . . . . . . . . . . . 19 ..^
293 elioo2 11582 . . . . . . . . . . . . . . . . . . 19
294291, 292, 293syl2anc 661 . . . . . . . . . . . . . . . . . 18 ..^
295290, 294mpbird 232 . . . . . . . . . . . . . . . . 17 ..^
296258, 255syl 16 . . . . . . . . . . . . . . . . . . . 20
297254, 259sseldi 3507 . . . . . . . . . . . . . . . . . . . 20
298296, 297npcand 9946 . . . . . . . . . . . . . . . . . . 19
299298eqcomd 2475 . . . . . . . . . . . . . . . . . 18
300299adantlr 714 . . . . . . . . . . . . . . . . 17 ..^
301 oveq1 6302 . . . . . . . . . . . . . . . . . . 19
302301eqeq2d 2481 . . . . . . . . . . . . . . . . . 18
303302rspcev 3219 . . . . . . . . . . . . . . . . 17
304295, 300, 303syl2anc 661 . . . . . . . . . . . . . . . 16 ..^
305257, 304jca 532 . . . . . . . . . . . . . . 15 ..^
306305, 199sylibr 212 . . . . . . . . . . . . . 14 ..^
307306ex 434 . . . . . . . . . . . . 13 ..^
308252, 307impbid 191 . . . . . . . . . . . 12 ..^
309197, 308alrimi 1825 . . . . . . . . . . 11 ..^
310 dfcleq 2460 . . . . . . . . . . 11
311309, 310sylibr 212 . . . . . . . . . 10 ..^
312311reseq2d 5279 . . . . . . . . 9 ..^
31335adantr 465 . . . . . . . . . 10 ..^
314 ioossre 11598 . . . . . . . . . . 11
315314a1i 11 . . . . . . . . . 10 ..^
316313, 315feqresmpt 5928 . . . . . . . . 9 ..^
317312, 316eqtrd 2508 . . . . . . . 8 ..^
318311oveq1d 6310 . . . . . . . 8 ..^
319317, 318eleq12d 2549 . . . . . . 7 ..^
320196, 319mpbid 210 . . . . . 6 ..^
32157, 158syl5sseqr 3558 . . . . . . . . 9
322321adantr 465 . . . . . . . 8 ..^
323 eqid 2467 . . . . . . . 8
324 simpll 753 . . . . . . . . 9 ..^
325324, 182syl 16 . . . . . . . . . 10 ..^
326324, 184syl 16 . . . . . . . . . 10 ..^
327324, 186syl 16 . . . . . . . . . 10 ..^
328188adantr 465 . . . . . . . . . 10 ..^ ..^
329190, 212sseldi 3507 . . . . . . . . . 10 ..^
330325, 326, 327, 328, 329fourierdlem1 31731 . . . . . . . . 9 ..^
331 nfv 1683 . . . . . . . . . 10
332 eleq1 2539 . . . . . . . . . . . 12
333332anbi2d 703 . . . . . . . . . . 11
334 oveq1 6302 . . . . . . . . . . . . 13
335334fveq2d 5876 . . . . . . . . . . . 12
336 fveq2 5872 . . . . . . . . . . . 12
337335, 336eqeq12d 2489 . . . . . . . . . . 11
338333, 337imbi12d 320 . . . . . . . . . 10
339331, 338, 194chvar 1982 . . . . . . . . 9
340324, 330, 339syl2anc 661 . . . . . . . 8 ..^
341162, 142, 322, 264, 323, 179, 340, 64limcperiod 31493 . . . . . . 7 ..^ lim
342126eqcomd 2475 . . . . . . . 8 ..^
343317, 342oveq12d 6313 . . . . . . 7 ..^ lim lim
344341, 343eleqtrd 2557 . . . . . 6 ..^ lim
345162, 142, 322, 264, 323, 179, 340, 65limcperiod 31493 . . . . . . 7 ..^ lim
346114eqcomd 2475 . . . . . . . 8 ..^
347317, 346oveq12d 6313 . . . . . . 7 ..^ lim lim
348345, 347eleqtrd 2557 . . . . . 6 ..^ lim
349139, 140, 320, 344, 348iblcncfioo 31619 . . . . 5 ..^
350313adantr 465 . . . . . 6 ..^
351139adantr 465 . . . . . . 7 ..^
352140adantr 465 . . . . . . 7 ..^
353 simpr 461 . . . . . . 7 ..^
354 eliccre 31427 . . . . . . 7
355351, 352, 353, 354syl3anc 1228 . . . . . 6 ..^
356350, 355ffvelrnd 6033 . . . . 5 ..^
357139, 140, 349, 356ibliooicc 31612 . . . 4 ..^
35817, 24, 108, 128, 138, 357itgspltprt 31620 . . 3 ..^
359 fourierdlem81.g . . . . . . . . . . . . . . 15
360359a1i 11 . . . . . . . . . . . . . 14 ..^
361 iftrue 3951 . . . . . . . . . . . . . . . . . 18
362 iftrue 3951 . . . . . . . . . . . . . . . . . . 19
363362eqcomd 2475 . . . . . . . . . . . . . . . . . 18
364361, 363eqtrd 2508 . . . . . . . . . . . . . . . . 17
365364adantl 466 . . . . . . . . . . . . . . . 16 ..^
366 iffalse 3954 . . . . . . . . . . . . . . . . . . . 20
367366adantr 465 . . . . . . . . . . . . . . . . . . 19
368 iftrue 3951 . . . . . . . . . . . . . . . . . . . 20
369368adantl 466 . . . . . . . . . . . . . . . . . . 19
370 iffalse 3954 . . . . . . . . . . . . . . . . . . . . 21
371370adantr 465 . . . . . . . . . . . . . . . . . . . 20
372 iftrue 3951 . . . . . . . . . . . . . . . . . . . . 21
373372adantl 466 . . . . . . . . . . . . . . . . . . . 20
374371, 373eqtr2d 2509 . . . . . . . . . . . . . . . . . . 19
375367, 369, 374