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

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

Proof of Theorem fourierdlem92
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem92.a . . . 4
3 fourierdlem92.b . . . 4
5 fourierdlem92.p . . 3 ..^
6 fourierdlem92.m . . . 4
8 fourierdlem92.t . . . . 5
98adantr 465 . . . 4
10 simpr 461 . . . 4
119, 10elrpd 11279 . . 3
12 fourierdlem92.q . . . 4
14 fourierdlem92.fper . . . 4
16 fveq2 5872 . . . . 5
1716oveq1d 6311 . . . 4
1817cbvmptv 4548 . . 3
19 fourierdlem92.f . . . 4
21 fourierdlem92.cncf . . . 4 ..^
2221adantlr 714 . . 3 ..^
23 fourierdlem92.r . . . 4 ..^ lim
2423adantlr 714 . . 3 ..^ lim
25 fourierdlem92.l . . . 4 ..^ lim
2625adantlr 714 . . 3 ..^ lim
27 eqeq1 2461 . . . . 5
28 eqeq1 2461 . . . . . 6
29 fveq2 5872 . . . . . 6
3028, 29ifbieq2d 3969 . . . . 5
3127, 30ifbieq2d 3969 . . . 4
3231cbvmptv 4548 . . 3
33 eqid 2457 . . 3
342, 4, 5, 7, 11, 13, 15, 18, 20, 22, 24, 26, 32, 33fourierdlem81 32173 . 2
35 simpr 461 . . . . . . . 8
3635oveq2d 6312 . . . . . . 7
371recnd 9639 . . . . . . . . 9
3837adantr 465 . . . . . . . 8
3938addid1d 9797 . . . . . . 7
4036, 39eqtrd 2498 . . . . . 6
4135oveq2d 6312 . . . . . . 7
423recnd 9639 . . . . . . . . 9
4342adantr 465 . . . . . . . 8
4443addid1d 9797 . . . . . . 7
4541, 44eqtrd 2498 . . . . . 6
4640, 45oveq12d 6314 . . . . 5
4746itgeq1d 31958 . . . 4
49 simpll 753 . . . 4
50 simpr 461 . . . . . . 7
51 simplr 755 . . . . . . 7
52 ioran 490 . . . . . . 7
5350, 51, 52sylanbrc 664 . . . . . 6
5449, 8syl 16 . . . . . . 7
55 0red 9614 . . . . . . 7
5654, 55lttrid 9740 . . . . . 6
5753, 56mpbird 232 . . . . 5
5854lt0neg1d 10143 . . . . 5
5957, 58mpbid 210 . . . 4
601, 8readdcld 9640 . . . . . . . . . . . 12
6160recnd 9639 . . . . . . . . . . 11
628recnd 9639 . . . . . . . . . . 11
6361, 62negsubd 9956 . . . . . . . . . 10
6437, 62pncand 9951 . . . . . . . . . 10
6563, 64eqtrd 2498 . . . . . . . . 9
663, 8readdcld 9640 . . . . . . . . . . . 12
6766recnd 9639 . . . . . . . . . . 11
6867, 62negsubd 9956 . . . . . . . . . 10
6942, 62pncand 9951 . . . . . . . . . 10
7068, 69eqtrd 2498 . . . . . . . . 9
7165, 70oveq12d 6314 . . . . . . . 8
7271eqcomd 2465 . . . . . . 7
7372itgeq1d 31958 . . . . . 6
7473adantr 465 . . . . 5
751adantr 465 . . . . . . 7
768adantr 465 . . . . . . 7
7775, 76readdcld 9640 . . . . . 6
783adantr 465 . . . . . . 7
7978, 76readdcld 9640 . . . . . 6
80 eqid 2457 . . . . . 6 ..^ ..^
816adantr 465 . . . . . 6
8276renegcld 10007 . . . . . . 7
83 simpr 461 . . . . . . 7
8482, 83elrpd 11279 . . . . . 6
855fourierdlem2 32094 . . . . . . . . . . . . . . . . . 18 ..^
866, 85syl 16 . . . . . . . . . . . . . . . . 17 ..^
8712, 86mpbid 210 . . . . . . . . . . . . . . . 16 ..^
8887simpld 459 . . . . . . . . . . . . . . 15
89 elmapi 7459 . . . . . . . . . . . . . . 15
9088, 89syl 16 . . . . . . . . . . . . . 14
9190ffvelrnda 6032 . . . . . . . . . . . . 13
928adantr 465 . . . . . . . . . . . . 13
9391, 92readdcld 9640 . . . . . . . . . . . 12
94 fourierdlem92.s . . . . . . . . . . . 12
9593, 94fmptd 6056 . . . . . . . . . . 11
96 reex 9600 . . . . . . . . . . . . 13
9796a1i 11 . . . . . . . . . . . 12
98 ovex 6324 . . . . . . . . . . . . 13
9998a1i 11 . . . . . . . . . . . 12
10097, 99elmapd 7452 . . . . . . . . . . 11
10195, 100mpbird 232 . . . . . . . . . 10
10294a1i 11 . . . . . . . . . . . . 13
103 fveq2 5872 . . . . . . . . . . . . . . 15
104103oveq1d 6311 . . . . . . . . . . . . . 14
105104adantl 466 . . . . . . . . . . . . 13
106 0zd 10897 . . . . . . . . . . . . . . . 16
1076nnzd 10989 . . . . . . . . . . . . . . . 16
108106, 107, 1063jca 1176 . . . . . . . . . . . . . . 15
109 0le0 10646 . . . . . . . . . . . . . . . 16
110109a1i 11 . . . . . . . . . . . . . . 15
111 nnnn0 10823 . . . . . . . . . . . . . . . . 17
112111nn0ge0d 10876 . . . . . . . . . . . . . . . 16
1136, 112syl 16 . . . . . . . . . . . . . . 15
114108, 110, 113jca32 535 . . . . . . . . . . . . . 14
115 elfz2 11704 . . . . . . . . . . . . . 14
116114, 115sylibr 212 . . . . . . . . . . . . 13
11790, 116ffvelrnd 6033 . . . . . . . . . . . . . 14
118117, 8readdcld 9640 . . . . . . . . . . . . 13
119102, 105, 116, 118fvmptd 5961 . . . . . . . . . . . 12
120 simprll 763 . . . . . . . . . . . . . 14 ..^
12187, 120syl 16 . . . . . . . . . . . . 13
122121oveq1d 6311 . . . . . . . . . . . 12
123119, 122eqtrd 2498 . . . . . . . . . . 11
124 fveq2 5872 . . . . . . . . . . . . . . 15
125124oveq1d 6311 . . . . . . . . . . . . . 14
126125adantl 466 . . . . . . . . . . . . 13
1276nnnn0d 10873 . . . . . . . . . . . . . . 15
128 nn0uz 11140 . . . . . . . . . . . . . . 15
129127, 128syl6eleq 2555 . . . . . . . . . . . . . 14
130 eluzfz2 11719 . . . . . . . . . . . . . 14
131129, 130syl 16 . . . . . . . . . . . . 13
13290, 131ffvelrnd 6033 . . . . . . . . . . . . . 14
133132, 8readdcld 9640 . . . . . . . . . . . . 13
134102, 126, 131, 133fvmptd 5961 . . . . . . . . . . . 12
135 simprlr 764 . . . . . . . . . . . . . 14 ..^
13687, 135syl 16 . . . . . . . . . . . . 13
137136oveq1d 6311 . . . . . . . . . . . 12
138134, 137eqtrd 2498 . . . . . . . . . . 11
139123, 138jca 532 . . . . . . . . . 10
14090adantr 465 . . . . . . . . . . . . . 14 ..^
141 elfzofz 11841 . . . . . . . . . . . . . . 15 ..^
142141adantl 466 . . . . . . . . . . . . . 14 ..^
143140, 142ffvelrnd 6033 . . . . . . . . . . . . 13 ..^
144 fzofzp1 11912 . . . . . . . . . . . . . . 15 ..^
145144adantl 466 . . . . . . . . . . . . . 14 ..^
146140, 145ffvelrnd 6033 . . . . . . . . . . . . 13 ..^
1478adantr 465 . . . . . . . . . . . . 13 ..^
14887simprrd 758 . . . . . . . . . . . . . 14 ..^
149148r19.21bi 2826 . . . . . . . . . . . . 13 ..^
150143, 146, 147, 149ltadd1dd 10184 . . . . . . . . . . . 12 ..^
151143, 147readdcld 9640 . . . . . . . . . . . . 13 ..^
15294fvmpt2 5964 . . . . . . . . . . . . 13
153142, 151, 152syl2anc 661 . . . . . . . . . . . 12 ..^
15494, 18eqtr4i 2489 . . . . . . . . . . . . . 14
155154a1i 11 . . . . . . . . . . . . 13 ..^
156 fveq2 5872 . . . . . . . . . . . . . . 15
157156oveq1d 6311 . . . . . . . . . . . . . 14
158157adantl 466 . . . . . . . . . . . . 13 ..^
159146, 147readdcld 9640 . . . . . . . . . . . . 13 ..^
160155, 158, 145, 159fvmptd 5961 . . . . . . . . . . . 12 ..^
161150, 153, 1603brtr4d 4486 . . . . . . . . . . 11 ..^
162161ralrimiva 2871 . . . . . . . . . 10 ..^
163101, 139, 162jca32 535 . . . . . . . . 9 ..^
164 fourierdlem92.h . . . . . . . . . . 11 ..^
165164fourierdlem2 32094 . . . . . . . . . 10 ..^
1666, 165syl 16 . . . . . . . . 9 ..^
167163, 166mpbird 232 . . . . . . . 8
168164fveq1i 5873 . . . . . . . 8 ..^
169167, 168syl6eleq 2555 . . . . . . 7 ..^
170169adantr 465 . . . . . 6 ..^
17160adantr 465 . . . . . . . . . . . 12
17266adantr 465 . . . . . . . . . . . 12
173 simpr 461 . . . . . . . . . . . 12
174 eliccre 31743 . . . . . . . . . . . 12
175171, 172, 173, 174syl3anc 1228 . . . . . . . . . . 11
176175recnd 9639 . . . . . . . . . 10
17762negcld 9937 . . . . . . . . . . 11
178177adantr 465 . . . . . . . . . 10
179176, 178addcld 9632 . . . . . . . . 9
180 simpl 457 . . . . . . . . . 10
1811adantr 465 . . . . . . . . . . 11
1823adantr 465 . . . . . . . . . . 11
1838renegcld 10007 . . . . . . . . . . . . 13
184183adantr 465 . . . . . . . . . . . 12
185175, 184readdcld 9640 . . . . . . . . . . 11
18663, 64eqtr2d 2499 . . . . . . . . . . . . 13
187186adantr 465 . . . . . . . . . . . 12
188171rexrd 9660 . . . . . . . . . . . . . 14
189172rexrd 9660 . . . . . . . . . . . . . 14
190 iccgelb 11606 . . . . . . . . . . . . . 14
191188, 189, 173, 190syl3anc 1228 . . . . . . . . . . . . 13
192171, 175, 184, 191leadd1dd 10187 . . . . . . . . . . . 12
193187, 192eqbrtrd 4476 . . . . . . . . . . 11
194 iccleub 11605 . . . . . . . . . . . . . 14
195188, 189, 173, 194syl3anc 1228 . . . . . . . . . . . . 13
196175, 172, 184, 195leadd1dd 10187 . . . . . . . . . . . 12
197172recnd 9639 . . . . . . . . . . . . . 14
19862adantr 465 . . . . . . . . . . . . . 14
199197, 198negsubd 9956 . . . . . . . . . . . . 13
20069adantr 465 . . . . . . . . . . . . 13
201199, 200eqtrd 2498 . . . . . . . . . . . 12
202196, 201breqtrd 4480 . . . . . . . . . . 11
203181, 182, 185, 193, 202eliccd 31741 . . . . . . . . . 10
204180, 203jca 532 . . . . . . . . 9
205 eleq1 2529 . . . . . . . . . . . 12
206205anbi2d 703 . . . . . . . . . . 11
207 oveq1 6303 . . . . . . . . . . . . 13
208207fveq2d 5876 . . . . . . . . . . . 12
209 fveq2 5872 . . . . . . . . . . . 12
210208, 209eqeq12d 2479 . . . . . . . . . . 11
211206, 210imbi12d 320 . . . . . . . . . 10
212 eleq1 2529 . . . . . . . . . . . . 13
213212anbi2d 703 . . . . . . . . . . . 12
214 oveq1 6303 . . . . . . . . . . . . . 14
215214fveq2d 5876 . . . . . . . . . . . . 13
216 fveq2 5872 . . . . . . . . . . . . 13
217215, 216eqeq12d 2479 . . . . . . . . . . . 12
218213, 217imbi12d 320 . . . . . . . . . . 11
219218, 14chvarv 2015 . . . . . . . . . 10
220211, 219vtoclg 3167 . . . . . . . . 9
221179, 204, 220sylc 60 . . . . . . . 8
222176, 198negsubd 9956 . . . . . . . . . . 11
223222oveq1d 6311 . . . . . . . . . 10
224176, 198npcand 9954 . . . . . . . . . 10
225223, 224eqtrd 2498 . . . . . . . . 9
226225fveq2d 5876 . . . . . . . 8
227221, 226eqtr3d 2500 . . . . . . 7
228227adantlr 714 . . . . . 6
229 fveq2 5872 . . . . . . . 8
230229oveq1d 6311 . . . . . . 7
231230cbvmptv 4548 . . . . . 6
23219adantr 465 . . . . . 6
23319adantr 465 . . . . . . . . . 10 ..^
234 ioossre 11611 . . . . . . . . . . 11
235234a1i 11 . . . . . . . . . 10 ..^
236233, 235feqresmpt 5927 . . . . . . . . 9 ..^
237153, 160oveq12d 6314 . . . . . . . . . . 11 ..^
238143, 146, 147iooshift 31765 . . . . . . . . . . 11 ..^
239237, 238eqtrd 2498 . . . . . . . . . 10 ..^
240239mpteq1d 4538 . . . . . . . . 9 ..^
241 simpll 753 . . . . . . . . . . . . 13 ..^
242 simplr 755 . . . . . . . . . . . . 13 ..^ ..^
243238eleq2d 2527 . . . . . . . . . . . . . 14 ..^
244243biimpar 485 . . . . . . . . . . . . 13 ..^
245143rexrd 9660 . . . . . . . . . . . . . . 15 ..^
2462453adant3 1016 . . . . . . . . . . . . . 14 ..^
247146rexrd 9660 . . . . . . . . . . . . . . 15 ..^
2482473adant3 1016 . . . . . . . . . . . . . 14 ..^
249 elioore 11584 . . . . . . . . . . . . . . . . 17
250249adantl 466 . . . . . . . . . . . . . . . 16
2518adantr 465 . . . . . . . . . . . . . . . 16
252250, 251resubcld 10008 . . . . . . . . . . . . . . 15
2532523adant2 1015 . . . . . . . . . . . . . 14 ..^
254143recnd 9639 . . . . . . . . . . . . . . . . . 18 ..^
25562adantr 465 . . . . . . . . . . . . . . . . . 18 ..^
256254, 255pncand 9951 . . . . . . . . . . . . . . . . 17 ..^
257256eqcomd 2465 . . . . . . . . . . . . . . . 16 ..^
2582573adant3 1016 . . . . . . . . . . . . . . 15 ..^
2591513adant3 1016 . . . . . . . . . . . . . . . 16 ..^
2602503adant2 1015 . . . . . . . . . . . . . . . 16 ..^
26183ad2ant1 1017 . . . . . . . . . . . . . . . 16 ..^
262151rexrd 9660 . . . . . . . . . . . . . . . . . 18 ..^
2632623adant3 1016 . . . . . . . . . . . . . . . . 17 ..^
264159rexrd 9660 . . . . . . . . . . . . . . . . . 18 ..^
2652643adant3 1016 . . . . . . . . . . . . . . . . 17 ..^
266 simp3 998 . . . . . . . . . . . . . . . . 17 ..^
267 ioogtlb 31731 . . . . . . . . . . . . . . . . 17
268263, 265, 266, 267syl3anc 1228 . . . . . . . . . . . . . . . 16 ..^
269259, 260, 261, 268ltsub1dd 10185 . . . . . . . . . . . . . . 15 ..^
270258, 269eqbrtrd 4476 . . . . . . . . . . . . . 14 ..^
2711593adant3 1016 . . . . . . . . . . . . . . . 16 ..^
272 iooltub 31751 . . . . . . . . . . . . . . . . 17
273263, 265, 266, 272syl3anc 1228 . . . . . . . . . . . . . . . 16 ..^
274260, 271, 261, 273ltsub1dd 10185 . . . . . . . . . . . . . . 15 ..^
275146recnd 9639 . . . . . . . . . . . . . . . . 17 ..^
276275, 255pncand 9951 . . . . . . . . . . . . . . . 16 ..^
2772763adant3 1016 . . . . . . . . . . . . . . 15 ..^
278274, 277breqtrd 4480 . . . . . . . . . . . . . 14 ..^
279246, 248, 253, 270, 278eliood 31734 . . . . . . . . . . . . 13 ..^
280241, 242, 244, 279syl3anc 1228 . . . . . . . . . . . 12 ..^
281 fvres 5886 . . . . . . . . . . . 12
282280, 281syl 16 . . . . . . . . . . 11 ..^
283241, 244, 252syl2anc 661 . . . . . . . . . . . 12 ..^
28413ad2ant1 1017 . . . . . . . . . . . . . . 15 ..^
28533ad2ant1 1017 . . . . . . . . . . . . . . 15 ..^
28664eqcomd 2465 . . . . . . . . . . . . . . . . . 18
2872863ad2ant1 1017 . . . . . . . . . . . . . . . . 17 ..^
288603ad2ant1 1017 . . . . . . . . . . . . . . . . . 18 ..^
2891adantr 465 . . . . . . . . . . . . . . . . . . . . 21 ..^
2901rexrd 9660 . . . . . . . . . . . . . . . . . . . . . . 23
291290adantr 465 . . . . . . . . . . . . . . . . . . . . . 22 ..^
2923rexrd 9660 . . . . . . . . . . . . . . . . . . . . . . 23
293292adantr 465 . . . . . . . . . . . . . . . . . . . . . 22 ..^
2945, 6, 12fourierdlem15 32107 . . . . . . . . . . . . . . . . . . . . . . . 24
295294adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
296295, 142ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . 22 ..^
297 iccgelb 11606 . . . . . . . . . . . . . . . . . . . . . 22
298291, 293, 296, 297syl3anc 1228 . . . . . . . . . . . . . . . . . . . . 21 ..^
299289, 143, 147, 298leadd1dd 10187 . . . . . . . . . . . . . . . . . . . 20 ..^
3002993adant3 1016 . . . . . . . . . . . . . . . . . . 19 ..^
301288, 259, 260, 300, 268lelttrd 9757 . . . . . . . . . . . . . . . . . 18 ..^
302288, 260, 261, 301ltsub1dd 10185 . . . . . . . . . . . . . . . . 17 ..^
303287, 302eqbrtrd 4476 . . . . . . . . . . . . . . . 16 ..^
304284, 253, 303ltled 9750 . . . . . . . . . . . . . . 15 ..^
3051463adant3 1016 . . . . . . . . . . . . . . . . 17 ..^
306295, 145ffvelrnd 6033 . . . . . . . . . . . . . . . . . . 19 ..^
307 iccleub 11605 . . . . . . . . . . . . . . . . . . 19
308291, 293, 306, 307syl3anc 1228 . . . . . . . . . . . . . . . . . 18 ..^
3093083adant3 1016 . . . . . . . . . . . . . . . . 17 ..^
310253, 305, 285, 278, 309ltletrd 9759 . . . . . . . . . . . . . . . 16 ..^
311253, 285, 310ltled 9750 . . . . . . . . . . . . . . 15 ..^
312284, 285, 253, 304, 311eliccd 31741 . . . . . . . . . . . . . 14 ..^
313241, 242, 244, 312syl3anc 1228 . . . . . . . . . . . . 13 ..^
314241, 313jca 532 . . . . . . . . . . . 12 ..^
315 eleq1 2529 . . . . . . . . . . . . . . 15
316315anbi2d 703 . . . . . . . . . . . . . 14
317 oveq1 6303 . . . . . . . . . . . . . . . 16
318317fveq2d 5876 . . . . . . . . . . . . . . 15
319 fveq2 5872 . . . . . . . . . . . . . . 15
320318, 319eqeq12d 2479 . . . . . . . . . . . . . 14
321316, 320imbi12d 320 . . . . . . . . . . . . 13
322321, 219vtoclg 3167 . . . . . . . . . . . 12
323283, 314, 322sylc 60 . . . . . . . . . . 11 ..^
324244, 249syl 16 . . . . . . . . . . . 12 ..^
325 recn 9599 . . . . . . . . . . . . . . 15
326325adantl 466 . . . . . . . . . . . . . 14
32762adantr 465 . . . . . . . . . . . . . 14
328326, 327npcand 9954 . . . . . . . . . . . . 13
329328fveq2d 5876 . . . . . . . . . . . 12
330241, 324, 329syl2anc 661 . . . . . . . . . . 11 ..^
331282, 323, 3303eqtr2rd 2505 . . . . . . . . . 10 ..^
332331mpteq2dva 4543 . . . . . . . . 9 ..^
333236, 240, 3323eqtrd 2502 . . . . . . . 8 ..^
334 ioosscn 31730 . . . . . . . . . . 11
335334a1i 11 . . . . . . . . . 10 ..^
336 eqeq1 2461 . . . . . . . . . . . . 13
337336rexbidv 2968 . . . . . . . . . . . 12
338 oveq1 6303 . . . . . . . . . . . . . 14
339338eqeq2d 2471 . . . . . . . . . . . . 13
340339cbvrexv 3085 . . . . . . . . . . . 12
341337, 340syl6bb 261 . . . . . . . . . . 11
342341cbvrabv 3108 . . . . . . . . . 10
343 eqid 2457 . . . . . . . . . 10
344335, 255, 342, 21, 343cncfshift 31879 . . . . . . . . 9 ..^
345239eqcomd 2465 . . . . . . . . . 10 ..^
346345oveq1d 6311 . . . . . . . . 9 ..^
347344, 346eleqtrd 2547 . . . . . . . 8 ..^
348333, 347eqeltrd 2545 . . . . . . 7 ..^
349348adantlr 714 . . . . . 6 ..^
350 ffdm 5751 . . . . . . . . . . . 12
35119, 350syl 16 . . . . . . . . . . 11
352351simpld 459 . . . . . . . . . 10
353352adantr 465 . . . . . . . . 9 ..^
354 ioossre 11611 . . . . . . . . . 10
355 fdm 5741 . . . . . . . . . . 11
356233, 355syl 16 . . . . . . . . . 10 ..^
357354, 356syl5sseqr 3548 . . . . . . . . 9 ..^
358342eqcomi 2470 . . . . . . . . 9
359235, 345, 3563sstr4d 3542 . . . . . . . . . 10 ..^
360342, 359syl5eqssr 3544 . . . . . . . . 9 ..^
361 simpll 753 . . . . . . . . . 10 ..^
362361, 290syl 16 . . . . . . . . . . 11 ..^
363361, 292syl 16 . . . . . . . . . . 11 ..^
364361, 294syl 16 . . . . . . . . . . 11 ..^
365 simplr 755 . . . . . . . . . . 11 ..^ ..^
366 ioossicc 11635 . . . . . . . . . . . . 13
367366sseli 3495 . . . . . . . . . . . 12
368367adantl 466 . . . . . . . . . . 11 ..^
369362, 363, 364, 365, 368fourierdlem1 32093 . . . . . . . . . 10 ..^
370 eleq1 2529 . . . . . . . . . . . . 13
371370anbi2d 703 . . . . . . . . . . . 12
372 oveq1 6303 . . . . . . . . . . . . . 14
373372fveq2d 5876 . . . . . . . . . . . . 13
374 fveq2 5872 . . . . . . . . . . . . 13
375373, 374eqeq12d 2479 . . . . . . . . . . . 12
376371, 375imbi12d 320 . . . . . . . . . . 11
377376, 14chvarv 2015 . . . . . . . . . 10
378361, 369, 377syl2anc 661 . . . . . . . . 9 ..^
379353, 335, 357, 255, 358, 360, 378, 23limcperiod 31837 . . . . . . . 8 ..^ lim
380358, 345syl5eq 2510 . . . . . . . . . 10 ..^
381380reseq2d 5283 . . . . . . . . 9 ..^
382153eqcomd 2465 . . . . . . . . 9 ..^
383381, 382oveq12d 6314 . . . . . . . 8 ..^ lim lim
384379, 383eleqtrd 2547 . . . . . . 7 ..^ lim
385384adantlr 714 . . . . . 6 ..^ lim
386353, 335, 357, 255, 358, 360, 378, 25limcperiod 31837 . . . . . . . 8 ..^ lim
387160eqcomd 2465 . . . . . . . . 9 ..^
388381, 387oveq12d 6314 . . . . . . . 8 ..^ lim lim
389386, 388eleqtrd 2547 . . . . . . 7 ..^ lim
390389adantlr 714 . . . . . 6 ..^ lim
391 eqeq1 2461 . . . . . . . 8
392 eqeq1 2461 . . . . . . . . 9
393392, 29ifbieq2d 3969 . . . . . . . 8
394391, 393ifbieq2d 3969 . . . . . . 7
395394cbvmptv 4548 . . . . . 6
396 eqid 2457 . . . . . 6
39777, 79, 80, 81, 84, 170, 228, 231, 232, 349, 385, 390, 395, 396fourierdlem81 32173 . . . . 5
39874, 397eqtr2d 2499 . . . 4
39949, 59, 398syl2anc 661 . . 3
40048, 399pm2.61dan 791 . 2
40134, 400pm2.61dan 791 1
 Colors of variables: wff setvar class Syntax hints: