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

Theorem fourierdlem74 31804
 Description: Given a piecewise smooth function , the derived function has a limit at the upper bound of each interval of the partition . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem74.xre
fourierdlem74.p ..^
fourierdlem74.f
fourierdlem74.x
fourierdlem74.y
fourierdlem74.w lim
fourierdlem74.h
fourierdlem74.m
fourierdlem74.v
fourierdlem74.r ..^ lim
fourierdlem74.q
fourierdlem74.o ..^
fourierdlem74.g
fourierdlem74.gcn ..^
fourierdlem74.e lim
fourierdlem74.a
Assertion
Ref Expression
fourierdlem74 ..^ lim
Distinct variable groups:   ,   ,   ,   ,,,   ,,   ,,   ,   ,   ,,   ,   ,   ,,,   ,   ,   ,,
Allowed substitution hints:   (,)   (,,,)   (,,,)   ()   (,,)   (,,)   (,,)   (,,,)   (,,)   (,,,)   ()   (,,)   (,,)

Proof of Theorem fourierdlem74
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfzofz 11823 . . . . . . 7 ..^
21adantl 466 . . . . . 6 ..^
3 pire 22718 . . . . . . . . . . . . 13
43renegcli 9892 . . . . . . . . . . . 12
54a1i 11 . . . . . . . . . . 11
6 fourierdlem74.xre . . . . . . . . . . 11
75, 6jca 532 . . . . . . . . . 10
8 readdcl 9587 . . . . . . . . . 10
97, 8syl 16 . . . . . . . . 9
103a1i 11 . . . . . . . . . . 11
1110, 6jca 532 . . . . . . . . . 10
12 readdcl 9587 . . . . . . . . . 10
1311, 12syl 16 . . . . . . . . 9
149, 13iccssred 31426 . . . . . . . 8
1514adantr 465 . . . . . . 7
16 fourierdlem74.p . . . . . . . . 9 ..^
17 fourierdlem74.m . . . . . . . . 9
18 fourierdlem74.v . . . . . . . . 9
1916, 17, 18fourierdlem15 31745 . . . . . . . 8
2019ffvelrnda 6032 . . . . . . 7
2115, 20sseldd 3510 . . . . . 6
222, 21syldan 470 . . . . 5 ..^
2322adantr 465 . . . 4 ..^
246adantr 465 . . . . 5 ..^
2524adantr 465 . . . 4 ..^
2616fourierdlem2 31732 . . . . . . . . . . 11 ..^
2717, 26syl 16 . . . . . . . . . 10 ..^
2818, 27mpbid 210 . . . . . . . . 9 ..^
2928simprd 463 . . . . . . . 8 ..^
3029simprd 463 . . . . . . 7 ..^
3130r19.21bi 2836 . . . . . 6 ..^
3231adantr 465 . . . . 5 ..^
33 eqcom 2476 . . . . . . 7
3433biimpi 194 . . . . . 6
3534adantl 466 . . . . 5 ..^
3632, 35breqtrrd 4479 . . . 4 ..^
37 fourierdlem74.f . . . . . 6
38 ioossre 11598 . . . . . . 7
3938a1i 11 . . . . . 6
4037, 39fssresd 5758 . . . . 5
4140ad2antrr 725 . . . 4 ..^
42 limcresi 22157 . . . . . . . 8 lim lim
43 fourierdlem74.w . . . . . . . 8 lim
4442, 43sseldi 3507 . . . . . . 7 lim
4544adantr 465 . . . . . 6 ..^ lim
46 mnfxr 11335 . . . . . . . . . 10
4746a1i 11 . . . . . . . . 9 ..^
4822rexrd 9655 . . . . . . . . . 10 ..^
4922mnfltd 31391 . . . . . . . . . 10 ..^
5047, 48, 49xrltled 31356 . . . . . . . . 9 ..^
51 iooss1 11576 . . . . . . . . 9
5247, 50, 51syl2anc 661 . . . . . . . 8 ..^
5352resabs1d 5309 . . . . . . 7 ..^
5453oveq1d 6310 . . . . . 6 ..^ lim lim
5545, 54eleqtrd 2557 . . . . 5 ..^ lim
5655adantr 465 . . . 4 ..^ lim
57 eqid 2467 . . . 4
58 ax-resscn 9561 . . . . . . . . . 10
5958a1i 11 . . . . . . . . 9
60 fss 5745 . . . . . . . . . 10
6137, 59, 60syl2anc 661 . . . . . . . . 9
62 ssid 3528 . . . . . . . . . 10
6362a1i 11 . . . . . . . . 9
64 eqid 2467 . . . . . . . . . 10 fld fld
6564tgioo2 21176 . . . . . . . . . 10 fldt
6664, 65dvres 22183 . . . . . . . . 9
6759, 61, 63, 39, 66syl22anc 1229 . . . . . . . 8
68 fourierdlem74.g . . . . . . . . . . 11
6968eqcomi 2480 . . . . . . . . . 10
70 iooretop 21141 . . . . . . . . . . 11
71 retop 21136 . . . . . . . . . . . 12
72 uniretop 21137 . . . . . . . . . . . . 13
7372isopn3 19435 . . . . . . . . . . . 12
7471, 38, 73mp2an 672 . . . . . . . . . . 11
7570, 74mpbi 208 . . . . . . . . . 10
7669, 75reseq12i 5277 . . . . . . . . 9
7776a1i 11 . . . . . . . 8
7867, 77eqtrd 2508 . . . . . . 7
7978dmeqd 5211 . . . . . 6
8079ad2antrr 725 . . . . 5 ..^
81 fourierdlem74.gcn . . . . . . . 8 ..^
8281adantr 465 . . . . . . 7 ..^
83 oveq2 6303 . . . . . . . . . 10
8483reseq2d 5279 . . . . . . . . 9
8584, 83feq12d 5726 . . . . . . . 8
8685adantl 466 . . . . . . 7 ..^
8782, 86mpbid 210 . . . . . 6 ..^
88 fdm 5741 . . . . . 6
8987, 88syl 16 . . . . 5 ..^
9080, 89eqtrd 2508 . . . 4 ..^
91 limcresi 22157 . . . . . . . . 9 lim lim
9291a1i 11 . . . . . . . 8 ..^ lim lim
9352resabs1d 5309 . . . . . . . . 9 ..^
9493oveq1d 6310 . . . . . . . 8 ..^ lim lim
9592, 94sseqtrd 3545 . . . . . . 7 ..^ lim lim
96 fourierdlem74.e . . . . . . . 8 lim
9796adantr 465 . . . . . . 7 ..^ lim
9895, 97sseldd 3510 . . . . . 6 ..^ lim
9967, 77eqtr2d 2509 . . . . . . . 8
10099oveq1d 6310 . . . . . . 7 lim lim
101100adantr 465 . . . . . 6 ..^ lim lim
10298, 101eleqtrd 2557 . . . . 5 ..^ lim
103102adantr 465 . . . 4 ..^ lim
104 eqid 2467 . . . 4
105 oveq2 6303 . . . . . . 7
106105fveq2d 5876 . . . . . 6
107106oveq1d 6310 . . . . 5
108107cbvmptv 4544 . . . 4
109 id 22 . . . . 5
110109cbvmptv 4544 . . . 4
11123, 25, 36, 41, 56, 57, 90, 103, 104, 108, 110fourierdlem60 31790 . . 3 ..^ lim
112 fourierdlem74.a . . . . . 6
113 iftrue 3951 . . . . . 6
114112, 113syl5eq 2520 . . . . 5
115114adantl 466 . . . 4 ..^
116 fourierdlem74.h . . . . . . . 8
117116reseq1i 5275 . . . . . . 7
118117a1i 11 . . . . . 6 ..^
119 ioossicc 11622 . . . . . . . . . 10
120119a1i 11 . . . . . . . . 9 ..^
1214rexri 9658 . . . . . . . . . . 11
122121a1i 11 . . . . . . . . . 10 ..^
1233rexri 9658 . . . . . . . . . . 11
124123a1i 11 . . . . . . . . . 10 ..^
1254a1i 11 . . . . . . . . . . . . 13
1263a1i 11 . . . . . . . . . . . . 13
1276adantr 465 . . . . . . . . . . . . . 14
12821, 127resubcld 9999 . . . . . . . . . . . . 13
1295recnd 9634 . . . . . . . . . . . . . . . . 17
1306recnd 9634 . . . . . . . . . . . . . . . . 17
131129, 130pncand 9943 . . . . . . . . . . . . . . . 16
132131eqcomd 2475 . . . . . . . . . . . . . . 15
133132adantr 465 . . . . . . . . . . . . . 14
1349adantr 465 . . . . . . . . . . . . . . . . . 18
13513adantr 465 . . . . . . . . . . . . . . . . . 18
136 elicc2 11601 . . . . . . . . . . . . . . . . . 18
137134, 135, 136syl2anc 661 . . . . . . . . . . . . . . . . 17
13820, 137mpbid 210 . . . . . . . . . . . . . . . 16
139138simp2d 1009 . . . . . . . . . . . . . . 15
140134, 21, 127lesub1d 10171 . . . . . . . . . . . . . . 15
141139, 140mpbid 210 . . . . . . . . . . . . . 14
142133, 141eqbrtrd 4473 . . . . . . . . . . . . 13
143138simp3d 1010 . . . . . . . . . . . . . . 15
14421, 135, 127lesub1d 10171 . . . . . . . . . . . . . . 15
145143, 144mpbid 210 . . . . . . . . . . . . . 14
146126recnd 9634 . . . . . . . . . . . . . . 15
147130adantr 465 . . . . . . . . . . . . . . 15
148146, 147pncand 9943 . . . . . . . . . . . . . 14
149145, 148breqtrd 4477 . . . . . . . . . . . . 13
150125, 126, 128, 142, 149eliccd 31425 . . . . . . . . . . . 12
151 fourierdlem74.q . . . . . . . . . . . 12
152150, 151fmptd 6056 . . . . . . . . . . 11
153152adantr 465 . . . . . . . . . 10 ..^
154 simpr 461 . . . . . . . . . 10 ..^ ..^
155122, 124, 153, 154fourierdlem8 31738 . . . . . . . . 9 ..^
156120, 155sstrd 3519 . . . . . . . 8 ..^
157 resmpt 5329 . . . . . . . 8
158156, 157syl 16 . . . . . . 7 ..^
159158adantr 465 . . . . . 6 ..^
1602, 128syldan 470 . . . . . . . . . 10 ..^
161151fvmpt2 5964 . . . . . . . . . 10
1622, 160, 161syl2anc 661 . . . . . . . . 9 ..^
163162adantr 465 . . . . . . . 8 ..^
164 fveq2 5872 . . . . . . . . . . . . . . 15
165164oveq1d 6310 . . . . . . . . . . . . . 14
166165cbvmptv 4544 . . . . . . . . . . . . 13
167151, 166eqtri 2496 . . . . . . . . . . . 12
168167a1i 11 . . . . . . . . . . 11 ..^
169 fveq2 5872 . . . . . . . . . . . . 13
170169oveq1d 6310 . . . . . . . . . . . 12
171170adantl 466 . . . . . . . . . . 11 ..^
172 fzofzp1 11889 . . . . . . . . . . . 12 ..^
173172adantl 466 . . . . . . . . . . 11 ..^
174 simpl 457 . . . . . . . . . . . . . 14 ..^
17528simpld 459 . . . . . . . . . . . . . . 15
176 elmapi 7452 . . . . . . . . . . . . . . 15
177175, 176syl 16 . . . . . . . . . . . . . 14
178174, 177syl 16 . . . . . . . . . . . . 13 ..^
179178, 173ffvelrnd 6033 . . . . . . . . . . . 12 ..^
180179, 24resubcld 9999 . . . . . . . . . . 11 ..^
181168, 171, 173, 180fvmptd 5962 . . . . . . . . . 10 ..^
182181adantr 465 . . . . . . . . 9 ..^
183 oveq1 6302 . . . . . . . . . 10
184183adantl 466 . . . . . . . . 9 ..^
185130ad2antrr 725 . . . . . . . . . . 11
186185subidd 9930 . . . . . . . . . 10
1871, 186sylanl2 651 . . . . . . . . 9 ..^
188182, 184, 1873eqtrd 2512 . . . . . . . 8 ..^
189163, 188oveq12d 6313 . . . . . . 7 ..^
190 id 22 . . . . . . . . . . . 12
191190ad2antlr 726 . . . . . . . . . . 11 ..^
192174anim1i 568 . . . . . . . . . . . . 13 ..^
193 simplr 754 . . . . . . . . . . . . 13 ..^ ..^
194 fourierdlem74.o . . . . . . . . . . . . . 14 ..^
19517adantr 465 . . . . . . . . . . . . . 14
1965, 10, 6, 16, 194, 17, 18, 151fourierdlem14 31744 . . . . . . . . . . . . . . 15
197196adantr 465 . . . . . . . . . . . . . 14
198 simpr 461 . . . . . . . . . . . . . . 15
199 fourierdlem74.x . . . . . . . . . . . . . . . . . . 19
200 ffn 5737 . . . . . . . . . . . . . . . . . . . . 21
20119, 200syl 16 . . . . . . . . . . . . . . . . . . . 20
202 fvelrnb 5921 . . . . . . . . . . . . . . . . . . . 20
203201, 202syl 16 . . . . . . . . . . . . . . . . . . 19
204199, 203mpbid 210 . . . . . . . . . . . . . . . . . 18
205 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23
206151fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . . . 23
207205, 150, 206syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22
208207adantr 465 . . . . . . . . . . . . . . . . . . . . 21
209 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . 22
210209adantl 466 . . . . . . . . . . . . . . . . . . . . 21
211130subidd 9930 . . . . . . . . . . . . . . . . . . . . . 22
212211ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21
213208, 210, 2123eqtrd 2512 . . . . . . . . . . . . . . . . . . . 20
214213ex 434 . . . . . . . . . . . . . . . . . . 19
215214reximdva 2942 . . . . . . . . . . . . . . . . . 18
216204, 215mpd 15 . . . . . . . . . . . . . . . . 17
217128, 151fmptd 6056 . . . . . . . . . . . . . . . . . . 19
218 ffn 5737 . . . . . . . . . . . . . . . . . . 19
219217, 218syl 16 . . . . . . . . . . . . . . . . . 18
220 fvelrnb 5921 . . . . . . . . . . . . . . . . . 18
221219, 220syl 16 . . . . . . . . . . . . . . . . 17
222216, 221mpbird 232 . . . . . . . . . . . . . . . 16
223222adantr 465 . . . . . . . . . . . . . . 15
224198, 223eqeltrd 2555 . . . . . . . . . . . . . 14
225194, 195, 197, 224fourierdlem12 31742 . . . . . . . . . . . . 13 ..^
226192, 193, 225syl2anc 661 . . . . . . . . . . . 12 ..^
227226adantlr 714 . . . . . . . . . . 11 ..^
228191, 227pm2.65da 576 . . . . . . . . . 10 ..^
229228adantlr 714 . . . . . . . . 9 ..^
230229iffalsed 3956 . . . . . . . 8 ..^
231 elioore 11571 . . . . . . . . . . . . . 14
232231adantl 466 . . . . . . . . . . . . 13 ..^
233 0re 9608 . . . . . . . . . . . . . 14
234233a1i 11 . . . . . . . . . . . . 13 ..^
235 elioo3g 11570 . . . . . . . . . . . . . . . . . . . . 21
236235biimpi 194 . . . . . . . . . . . . . . . . . . . 20
237236simpld 459 . . . . . . . . . . . . . . . . . . 19
238237simp1d 1008 . . . . . . . . . . . . . . . . . 18
239237simp2d 1009 . . . . . . . . . . . . . . . . . 18
240 elioo2 11582 . . . . . . . . . . . . . . . . . 18
241238, 239, 240syl2anc 661 . . . . . . . . . . . . . . . . 17
242190, 241mpbid 210 . . . . . . . . . . . . . . . 16
243242simp3d 1010 . . . . . . . . . . . . . . 15
244243adantl 466 . . . . . . . . . . . . . 14 ..^
245188adantr 465 . . . . . . . . . . . . . 14 ..^
246244, 245breqtrd 4477 . . . . . . . . . . . . 13 ..^
247232, 234, 246ltled 9744 . . . . . . . . . . . 12 ..^
248232, 234lenltd 9742 . . . . . . . . . . . 12 ..^
249247, 248mpbid 210 . . . . . . . . . . 11 ..^
250249iffalsed 3956 . . . . . . . . . 10 ..^
251250oveq2d 6311 . . . . . . . . 9 ..^
252251oveq1d 6310 . . . . . . . 8 ..^
25348ad2antrr 725 . . . . . . . . . . . 12 ..^
2546rexrd 9655 . . . . . . . . . . . . 13
255254ad3antrrr 729 . . . . . . . . . . . 12 ..^
25625adantr 465 . . . . . . . . . . . . 13 ..^
257256, 232readdcld 9635 . . . . . . . . . . . 12 ..^
258130adantr 465 . . . . . . . . . . . . . . . . 17 ..^
259 iccssre 11618 . . . . . . . . . . . . . . . . . . . . 21
2604, 3, 259mp2an 672 . . . . . . . . . . . . . . . . . . . 20
261260, 58sstri 3518 . . . . . . . . . . . . . . . . . . 19
262261a1i 11 . . . . . . . . . . . . . . . . . 18 ..^
263207, 150eqeltrd 2555 . . . . . . . . . . . . . . . . . . 19
264174, 2, 263syl2anc 661 . . . . . . . . . . . . . . . . . 18 ..^
265262, 264sseldd 3510 . . . . . . . . . . . . . . . . 17 ..^
266258, 265addcomd 9793 . . . . . . . . . . . . . . . 16 ..^
267162oveq1d 6310 . . . . . . . . . . . . . . . 16 ..^
26858, 22sseldi 3507 . . . . . . . . . . . . . . . . 17 ..^
269268, 258npcand 9946 . . . . . . . . . . . . . . . 16 ..^
270266, 267, 2693eqtrrd 2513 . . . . . . . . . . . . . . 15 ..^
271270adantr 465 . . . . . . . . . . . . . 14 ..^
272162, 160eqeltrd 2555 . . . . . . . . . . . . . . . 16 ..^
273272adantr 465 . . . . . . . . . . . . . . 15 ..^
274231adantl 466 . . . . . . . . . . . . . . 15 ..^
2756adantr 465 . . . . . . . . . . . . . . . 16
276174, 275sylan 471 . . . . . . . . . . . . . . 15 ..^
277242simp2d 1009 . . . . . . . . . . . . . . . 16
278277adantl 466 . . . . . . . . . . . . . . 15 ..^
279273, 274, 276, 278ltadd2dd 9752 . . . . . . . . . . . . . 14 ..^
280271, 279eqbrtrd 4473 . . . . . . . . . . . . 13 ..^
281280adantlr 714 . . . . . . . . . . . 12 ..^
282 ltaddneg 31384 . . . . . . . . . . . . . 14
283232, 256, 282syl2anc 661 . . . . . . . . . . . . 13 ..^
284246, 283mpbid 210 . . . . . . . . . . . 12 ..^
285253, 255, 257, 281, 284eliood 31418 . . . . . . . . . . 11 ..^
286 fvres 5886 . . . . . . . . . . . 12
287286eqcomd 2475 . . . . . . . . . . 11
288285, 287syl 16 . . . . . . . . . 10 ..^
289288oveq1d 6310 . . . . . . . . 9 ..^
290289oveq1d 6310 . . . . . . . 8 ..^
291230, 252, 2903eqtrd 2512 . . . . . . 7 ..^
292189, 291mpteq12dva 4530 . . . . . 6 ..^
293118, 159, 2923eqtrd 2512 . . . . 5 ..^
294293, 188oveq12d 6313 . . . 4 ..^ lim lim
295115, 294eleq12d 2549 . . 3 ..^ lim lim
296111, 295mpbird 232 . 2 ..^ lim
297 eqid 2467 . . . . 5
298 eqid 2467 . . . . 5
299 eqid 2467 . . . . 5
30037adantr 465 . . . . . . . . . 10
301231adantl 466 . . . . . . . . . . 11
302275, 301readdcld 9635 . . . . . . . . . 10
303300, 302ffvelrnd 6033 . . . . . . . . 9
30458, 303sseldi 3507 . . . . . . . 8
305304adantlr 714 . . . . . . 7 ..^
3063053adantl3 1154 . . . . . 6 ..^
307 fourierdlem74.y . . . . . . . . . 10
30858sseli 3505 . . . . . . . . . 10
309307, 308syl 16 . . . . . . . . 9
310 limccl 22147 . . . . . . . . . 10 lim
311310, 43sseldi 3507 . . . . . . . . 9
312309, 311ifcld 3988 . . . . . . . 8
313312adantr 465 . . . . . . 7
3143133ad2antl1 1158 . . . . . 6 ..^
315306, 314subcld 9942 . . . . 5 ..^
316231recnd 9634 . . . . . . 7
317316adantl 466 . . . . . 6 ..^
318228neqned 2670 . . . . . . . . 9 ..^
319318neneqd 2669 . . . . . . . 8 ..^
320 elsn 4047 . . . . . . . 8
321319, 320sylnibr 305 . . . . . . 7 ..^
3223213adantl3 1154 . . . . . 6 ..^
323317, 322eldifd 3492 . . . . 5 ..^
324 eqid 2467 . . . . . . . . . 10
325 eqid 2467 . . . . . . . . . 10
326 eqid 2467 . . . . . . . . . 10
327311ad2antrr 725 . . . . . . . . . 10 ..^
328174, 37syl 16 . . . . . . . . . . 11 ..^
329231ssriv 3513 . . . . . . . . . . . 12
330329a1i 11 . . . . . . . . . . 11 ..^
33148adantr 465 . . . . . . . . . . . 12 ..^
332179rexrd 9655 . . . . . . . . . . . . 13 ..^
333332adantr 465 . . . . . . . . . . . 12 ..^
334302adantlr 714 . . . . . . . . . . . 12 ..^
335217adantr 465 . . . . . . . . . . . . . . . 16 ..^
336335, 173ffvelrnd 6033 . . . . . . . . . . . . . . 15 ..^
337336adantr 465 . . . . . . . . . . . . . 14 ..^
338243adantl 466 . . . . . . . . . . . . . 14 ..^
339274, 337, 276, 338ltadd2dd 9752 . . . . . . . . . . . . 13 ..^
340181oveq2d 6311 . . . . . . . . . . . . . . 15 ..^
34158, 179sseldi 3507 . . . . . . . . . . . . . . . 16 ..^
342258, 341pncan3d 9945 . . . . . . . . . . . . . . 15 ..^
343 eqidd 2468 . . . . . . . . . . . . . . 15 ..^
344340, 342, 3433eqtrd 2512 . . . . . . . . . . . . . 14 ..^
345344adantr 465 . . . . . . . . . . . . 13 ..^
346339, 345breqtrd 4477 . . . . . . . . . . . 12 ..^
347331, 333, 334, 280, 346eliood 31418 . . . . . . . . . . 11 ..^
348 ioossre 11598 . . . . . . . . . . . 12
349348a1i 11 . . . . . . . . . . 11 ..^
350274, 338ltned 9732 . . . . . . . . . . 11 ..^
351 fourierdlem74.r . . . . . . . . . . . 12 ..^ lim
352344eqcomd 2475 . . . . . . . . . . . . 13 ..^
353352oveq2d 6311 . . . . . . . . . . . 12 ..^ lim lim
354351, 353eleqtrd 2557 . . . . . . . . . . 11 ..^ lim
355336recnd 9634 . . . . . . . . . . 11 ..^
356328, 24, 330, 324, 347, 349, 350, 354, 355fourierdlem53 31783 . . . . . . . . . 10 ..^ lim
357 ioosscn 31414 . . . . . . . . . . . 12
358357a1i 11 . . . . . . . . . . 11 ..^
359174, 311syl 16 . . . . . . . . . . 11 ..^
360325, 358, 359, 355constlimc 31489 . . . . . . . . . 10 ..^ lim
361324, 325, 326, 305, 327, 356, 360sublimc 31517 . . . . . . . . 9 ..^ lim
362361adantr 465 . . . . . . . 8 ..^ lim
363 iftrue 3951 . . . . . . . . . . 11
364363oveq2d 6311 . . . . . . . . . 10
365364adantl 466 . . . . . . . . 9 ..^
366231adantl 466 . . . . . . . . . . . . . . 15 ..^
367233a1i 11 . . . . . . . . . . . . . . 15 ..^
368337adantlr 714 . . . . . . . . . . . . . . . 16 ..^
369243adantl 466 . . . . . . . . . . . . . . . 16 ..^
370181adantr 465 . . . . . . . . . . . . . . . . . 18 ..^
371179adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
37224adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
373 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
374371, 372, 373ltled 9744 . . . . . . . . . . . . . . . . . . . . . 22 ..^
375374ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 ..^
376 simplr 754 . . . . . . . . . . . . . . . . . . . . 21 ..^
377375, 376condan 792 . . . . . . . . . . . . . . . . . . . 20 ..^
37816, 17, 18, 199fourierdlem12 31742 . . . . . . . . . . . . . . . . . . . . . 22 ..^
379378adantr 465 . . . . . . . . . . . . . . . . . . . . 21 ..^
380379adantr 465 . . . . . . . . . . . . . . . . . . . 20 ..^
381377, 380condan 792 . . . . . . . . . . . . . . . . . . 19 ..^
382371, 372suble0d 10155 . . . . . . . . . . . . . . . . . . 19 ..^
383381, 382mpbird 232 . . . . . . . . . . . . . . . . . 18 ..^
384370, 383eqbrtrd 4473 . . . . . . . . . . . . . . . . 17 ..^
385384adantr 465 . . . . . . . . . . . . . . . 16