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

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

Proof of Theorem fourierdlem75
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem75.xre . . . . . 6
21adantr 465 . . . . 5 ..^
32adantr 465 . . . 4 ..^
4 simpl 457 . . . . . . 7 ..^
5 fourierdlem75.v . . . . . . . . . 10
6 fourierdlem75.m . . . . . . . . . . 11
7 fourierdlem75.p . . . . . . . . . . . 12 ..^
87fourierdlem2 31732 . . . . . . . . . . 11 ..^
96, 8syl 16 . . . . . . . . . 10 ..^
105, 9mpbid 210 . . . . . . . . 9 ..^
1110simpld 459 . . . . . . . 8
12 elmapi 7452 . . . . . . . 8
1311, 12syl 16 . . . . . . 7
144, 13syl 16 . . . . . 6 ..^
15 fzofzp1 11889 . . . . . . 7 ..^
1615adantl 466 . . . . . 6 ..^
1714, 16ffvelrnd 6033 . . . . 5 ..^
1817adantr 465 . . . 4 ..^
19 eqcom 2476 . . . . . . 7
2019biimpi 194 . . . . . 6
2120adantl 466 . . . . 5 ..^
2210simprd 463 . . . . . . . 8 ..^
2322simprd 463 . . . . . . 7 ..^
2423r19.21bi 2836 . . . . . 6 ..^
2524adantr 465 . . . . 5 ..^
2621, 25eqbrtrd 4473 . . . 4 ..^
27 fourierdlem75.f . . . . . . 7
284, 27syl 16 . . . . . 6 ..^
29 ioossre 11598 . . . . . . 7
3029a1i 11 . . . . . 6 ..^
31 fssres 5757 . . . . . 6
3228, 30, 31syl2anc 661 . . . . 5 ..^
3332adantr 465 . . . 4 ..^
34 limcresi 22157 . . . . . . . 8 lim lim
35 fourierdlem75.y . . . . . . . 8 lim
3634, 35sseldi 3507 . . . . . . 7 lim
3736adantr 465 . . . . . 6 ..^ lim
38 pnfxr 11333 . . . . . . . . . 10
3938a1i 11 . . . . . . . . 9 ..^
4017rexrd 9655 . . . . . . . . . 10 ..^
41 ltpnf 11343 . . . . . . . . . . 11
4217, 41syl 16 . . . . . . . . . 10 ..^
4340, 39, 42xrltled 31356 . . . . . . . . 9 ..^
44 iooss2 11577 . . . . . . . . 9
4539, 43, 44syl2anc 661 . . . . . . . 8 ..^
46 resabs1 5308 . . . . . . . 8
4745, 46syl 16 . . . . . . 7 ..^
4847oveq1d 6310 . . . . . 6 ..^ lim lim
4937, 48eleqtrd 2557 . . . . 5 ..^ lim
5049adantr 465 . . . 4 ..^ lim
51 eqid 2467 . . . 4
52 ax-resscn 9561 . . . . . . . . . . 11
5352a1i 11 . . . . . . . . . 10
54 fss 5745 . . . . . . . . . . 11
5527, 53, 54syl2anc 661 . . . . . . . . . 10
56 ssid 3528 . . . . . . . . . . 11
5756a1i 11 . . . . . . . . . 10
5829a1i 11 . . . . . . . . . 10
59 eqid 2467 . . . . . . . . . . 11 fld fld
6059tgioo2 21176 . . . . . . . . . . 11 fldt
6159, 60dvres 22183 . . . . . . . . . 10
6253, 55, 57, 58, 61syl22anc 1229 . . . . . . . . 9
63 fourierdlem75.g . . . . . . . . . . . 12
6463eqcomi 2480 . . . . . . . . . . 11
65 iooretop 21141 . . . . . . . . . . . 12
66 retop 21136 . . . . . . . . . . . . 13
67 uniretop 21137 . . . . . . . . . . . . . 14
6867isopn3 19435 . . . . . . . . . . . . 13
6966, 29, 68mp2an 672 . . . . . . . . . . . 12
7065, 69mpbi 208 . . . . . . . . . . 11
7164, 70reseq12i 5277 . . . . . . . . . 10
7271a1i 11 . . . . . . . . 9
7362, 72eqtrd 2508 . . . . . . . 8
7473adantr 465 . . . . . . 7
7574dmeqd 5211 . . . . . 6
7675adantlr 714 . . . . 5 ..^
77 fourierdlem75.gcn . . . . . . . . 9 ..^
7877adantr 465 . . . . . . . 8 ..^
79 oveq1 6302 . . . . . . . . . . 11
8079reseq2d 5279 . . . . . . . . . 10
8180feq1d 5723 . . . . . . . . 9
8281adantl 466 . . . . . . . 8 ..^
8378, 82mpbid 210 . . . . . . 7 ..^
8479adantl 466 . . . . . . . 8 ..^
8584feq2d 5724 . . . . . . 7 ..^
8683, 85mpbid 210 . . . . . 6 ..^
87 fdm 5741 . . . . . 6
8886, 87syl 16 . . . . 5 ..^
8976, 88eqtrd 2508 . . . 4 ..^
90 limcresi 22157 . . . . . . . 8 lim lim
91 fourierdlem75.e . . . . . . . 8 lim
9290, 91sseldi 3507 . . . . . . 7 lim
9392adantr 465 . . . . . 6 ..^ lim
94 resabs1 5308 . . . . . . . . 9
9545, 94syl 16 . . . . . . . 8 ..^
964, 73syl 16 . . . . . . . . 9 ..^
9796eqcomd 2475 . . . . . . . 8 ..^
9895, 97eqtrd 2508 . . . . . . 7 ..^
9998oveq1d 6310 . . . . . 6 ..^ lim lim
10093, 99eleqtrd 2557 . . . . 5 ..^ lim
101100adantr 465 . . . 4 ..^ lim
102 eqid 2467 . . . 4
103 oveq2 6303 . . . . . . 7
104103fveq2d 5876 . . . . . 6
105104oveq1d 6310 . . . . 5
106105cbvmptv 4544 . . . 4
107 id 22 . . . . 5
108107cbvmptv 4544 . . . 4
1093, 18, 26, 33, 50, 51, 89, 101, 102, 106, 108fourierdlem61 31791 . . 3 ..^ lim
110 fourierdlem75.a . . . . . 6
111 iftrue 3951 . . . . . 6
112110, 111syl5eq 2520 . . . . 5
113112adantl 466 . . . 4 ..^
114 fourierdlem75.h . . . . . . . 8
115114reseq1i 5275 . . . . . . 7
116115a1i 11 . . . . . 6 ..^
117 ioossicc 11622 . . . . . . . . . 10
118117a1i 11 . . . . . . . . 9 ..^
119 pire 22718 . . . . . . . . . . . . 13
120119renegcli 9892 . . . . . . . . . . . 12
121120rexri 9658 . . . . . . . . . . 11
122121a1i 11 . . . . . . . . . 10 ..^
123119rexri 9658 . . . . . . . . . . 11
124123a1i 11 . . . . . . . . . 10 ..^
125120a1i 11 . . . . . . . . . . . . 13
126119a1i 11 . . . . . . . . . . . . 13
127120a1i 11 . . . . . . . . . . . . . . . . . . 19
128127, 1jca 532 . . . . . . . . . . . . . . . . . 18
129 readdcl 9587 . . . . . . . . . . . . . . . . . 18
130128, 129syl 16 . . . . . . . . . . . . . . . . 17
131119a1i 11 . . . . . . . . . . . . . . . . . . 19
132131, 1jca 532 . . . . . . . . . . . . . . . . . 18
133 readdcl 9587 . . . . . . . . . . . . . . . . . 18
134132, 133syl 16 . . . . . . . . . . . . . . . . 17
135130, 134iccssred 31426 . . . . . . . . . . . . . . . 16
136135adantr 465 . . . . . . . . . . . . . . 15
1377, 6, 5fourierdlem15 31745 . . . . . . . . . . . . . . . 16
138137ffvelrnda 6032 . . . . . . . . . . . . . . 15
139136, 138sseldd 3510 . . . . . . . . . . . . . 14
1401adantr 465 . . . . . . . . . . . . . 14
141139, 140resubcld 9999 . . . . . . . . . . . . 13
142127recnd 9634 . . . . . . . . . . . . . . . . 17
1431recnd 9634 . . . . . . . . . . . . . . . . 17
144142, 143pncand 9943 . . . . . . . . . . . . . . . 16
145144eqcomd 2475 . . . . . . . . . . . . . . 15
146145adantr 465 . . . . . . . . . . . . . 14
147130adantr 465 . . . . . . . . . . . . . . . . . 18
148134adantr 465 . . . . . . . . . . . . . . . . . 18
149 elicc2 11601 . . . . . . . . . . . . . . . . . 18
150147, 148, 149syl2anc 661 . . . . . . . . . . . . . . . . 17
151138, 150mpbid 210 . . . . . . . . . . . . . . . 16
152151simp2d 1009 . . . . . . . . . . . . . . 15
153147, 139, 140lesub1d 10171 . . . . . . . . . . . . . . 15
154152, 153mpbid 210 . . . . . . . . . . . . . 14
155146, 154eqbrtrd 4473 . . . . . . . . . . . . 13
156151simp3d 1010 . . . . . . . . . . . . . . 15
157139, 148, 140lesub1d 10171 . . . . . . . . . . . . . . 15
158156, 157mpbid 210 . . . . . . . . . . . . . 14
159126recnd 9634 . . . . . . . . . . . . . . 15
160143adantr 465 . . . . . . . . . . . . . . 15
161159, 160pncand 9943 . . . . . . . . . . . . . 14
162158, 161breqtrd 4477 . . . . . . . . . . . . 13
163125, 126, 141, 155, 162eliccd 31425 . . . . . . . . . . . 12
164 fourierdlem75.q . . . . . . . . . . . 12
165163, 164fmptd 6056 . . . . . . . . . . 11
166165adantr 465 . . . . . . . . . 10 ..^
167 simpr 461 . . . . . . . . . 10 ..^ ..^
168122, 124, 166, 167fourierdlem8 31738 . . . . . . . . 9 ..^
169118, 168sstrd 3519 . . . . . . . 8 ..^
170 resmpt 5329 . . . . . . . 8
171169, 170syl 16 . . . . . . 7 ..^
172171adantr 465 . . . . . 6 ..^
173 elfzofz 11823 . . . . . . . . 9 ..^
174 simpr 461 . . . . . . . . . . . 12
175164fvmpt2 5964 . . . . . . . . . . . 12
176174, 163, 175syl2anc 661 . . . . . . . . . . 11
177176adantr 465 . . . . . . . . . 10
178 oveq1 6302 . . . . . . . . . . 11
179178adantl 466 . . . . . . . . . 10
180143ad2antrr 725 . . . . . . . . . . 11
181180subidd 9930 . . . . . . . . . 10
182177, 179, 1813eqtrd 2512 . . . . . . . . 9
183173, 182sylanl2 651 . . . . . . . 8 ..^
184 fveq2 5872 . . . . . . . . . . . . . 14
185184oveq1d 6310 . . . . . . . . . . . . 13
186185cbvmptv 4544 . . . . . . . . . . . 12
187164, 186eqtri 2496 . . . . . . . . . . 11
188187a1i 11 . . . . . . . . . 10 ..^
189 fveq2 5872 . . . . . . . . . . . 12
190189oveq1d 6310 . . . . . . . . . . 11
191190adantl 466 . . . . . . . . . 10 ..^
19217, 2resubcld 9999 . . . . . . . . . 10 ..^
193188, 191, 16, 192fvmptd 5962 . . . . . . . . 9 ..^
194193adantr 465 . . . . . . . 8 ..^
195183, 194oveq12d 6313 . . . . . . 7 ..^
196 id 22 . . . . . . . . . . . 12
197196ad2antlr 726 . . . . . . . . . . 11 ..^
1984anim1i 568 . . . . . . . . . . . . 13 ..^
199 simplr 754 . . . . . . . . . . . . 13 ..^ ..^
200 fourierdlem75.o . . . . . . . . . . . . . 14 ..^
2016adantr 465 . . . . . . . . . . . . . 14
202127, 131, 1, 7, 200, 6, 5, 164fourierdlem14 31744 . . . . . . . . . . . . . . 15
203202adantr 465 . . . . . . . . . . . . . 14
204 simpr 461 . . . . . . . . . . . . . . 15
205 fourierdlem75.x . . . . . . . . . . . . . . . . . . 19
206 ffn 5737 . . . . . . . . . . . . . . . . . . . . 21
207137, 206syl 16 . . . . . . . . . . . . . . . . . . . 20
208 fvelrnb 5921 . . . . . . . . . . . . . . . . . . . 20
209207, 208syl 16 . . . . . . . . . . . . . . . . . . 19
210205, 209mpbid 210 . . . . . . . . . . . . . . . . . 18
211182ex 434 . . . . . . . . . . . . . . . . . . 19
212211reximdva 2942 . . . . . . . . . . . . . . . . . 18
213210, 212mpd 15 . . . . . . . . . . . . . . . . 17
214141, 164fmptd 6056 . . . . . . . . . . . . . . . . . . 19
215 ffn 5737 . . . . . . . . . . . . . . . . . . 19
216214, 215syl 16 . . . . . . . . . . . . . . . . . 18
217 fvelrnb 5921 . . . . . . . . . . . . . . . . . 18
218216, 217syl 16 . . . . . . . . . . . . . . . . 17
219213, 218mpbird 232 . . . . . . . . . . . . . . . 16
220219adantr 465 . . . . . . . . . . . . . . 15
221204, 220eqeltrd 2555 . . . . . . . . . . . . . 14
222200, 201, 203, 221fourierdlem12 31742 . . . . . . . . . . . . 13 ..^
223198, 199, 222syl2anc 661 . . . . . . . . . . . 12 ..^
224223adantlr 714 . . . . . . . . . . 11 ..^
225197, 224pm2.65da 576 . . . . . . . . . 10 ..^
226225adantlr 714 . . . . . . . . 9 ..^
227 iffalse 3954 . . . . . . . . 9
228226, 227syl 16 . . . . . . . 8 ..^
229183eqcomd 2475 . . . . . . . . . . . . 13 ..^
230229adantr 465 . . . . . . . . . . . 12 ..^
231 elioo3g 11570 . . . . . . . . . . . . . . . . . . 19
232231biimpi 194 . . . . . . . . . . . . . . . . . 18
233232simpld 459 . . . . . . . . . . . . . . . . 17
234233simp1d 1008 . . . . . . . . . . . . . . . 16
235233simp2d 1009 . . . . . . . . . . . . . . . 16
236 elioo2 11582 . . . . . . . . . . . . . . . 16
237234, 235, 236syl2anc 661 . . . . . . . . . . . . . . 15
238196, 237mpbid 210 . . . . . . . . . . . . . 14
239238simp2d 1009 . . . . . . . . . . . . 13
240239adantl 466 . . . . . . . . . . . 12 ..^
241230, 240eqbrtrd 4473 . . . . . . . . . . 11 ..^
242 iftrue 3951 . . . . . . . . . . 11
243241, 242syl 16 . . . . . . . . . 10 ..^
244243oveq2d 6311 . . . . . . . . 9 ..^
245244oveq1d 6310 . . . . . . . 8 ..^
2461rexrd 9655 . . . . . . . . . . . . . 14
247246ad3antrrr 729 . . . . . . . . . . . . 13 ..^
24840adantr 465 . . . . . . . . . . . . . 14 ..^
249248adantlr 714 . . . . . . . . . . . . 13 ..^
2503adantr 465 . . . . . . . . . . . . . 14 ..^
251 elioore 11571 . . . . . . . . . . . . . . 15
252251adantl 466 . . . . . . . . . . . . . 14 ..^
253250, 252readdcld 9635 . . . . . . . . . . . . 13 ..^
254252, 241elrpd 11266 . . . . . . . . . . . . . 14 ..^
255250, 254ltaddrpd 11297 . . . . . . . . . . . . 13 ..^
256251adantl 466 . . . . . . . . . . . . . . . 16 ..^
257214adantr 465 . . . . . . . . . . . . . . . . . 18 ..^
258257, 16ffvelrnd 6033 . . . . . . . . . . . . . . . . 17 ..^
259258adantr 465 . . . . . . . . . . . . . . . 16 ..^
2601adantr 465 . . . . . . . . . . . . . . . . 17
2614, 260sylan 471 . . . . . . . . . . . . . . . 16 ..^
262238simp3d 1010 . . . . . . . . . . . . . . . . 17
263262adantl 466 . . . . . . . . . . . . . . . 16 ..^
264256, 259, 261, 263ltadd2dd 9752 . . . . . . . . . . . . . . 15 ..^
265193oveq2d 6311 . . . . . . . . . . . . . . . . 17 ..^
266143adantr 465 . . . . . . . . . . . . . . . . . 18 ..^
26752, 17sseldi 3507 . . . . . . . . . . . . . . . . . 18 ..^
268266, 267pncan3d 9945 . . . . . . . . . . . . . . . . 17 ..^
269 eqidd 2468 . . . . . . . . . . . . . . . . 17 ..^
270265, 268, 2693eqtrd 2512 . . . . . . . . . . . . . . . 16 ..^
271270adantr 465 . . . . . . . . . . . . . . 15 ..^
272264, 271breqtrd 4477 . . . . . . . . . . . . . 14 ..^
273272adantlr 714 . . . . . . . . . . . . 13 ..^
274247, 249, 253, 255, 273eliood 31418 . . . . . . . . . . . 12 ..^
275 fvres 5886 . . . . . . . . . . . 12
276274, 275syl 16 . . . . . . . . . . 11 ..^
277276eqcomd 2475 . . . . . . . . . 10 ..^
278277oveq1d 6310 . . . . . . . . 9 ..^
279278oveq1d 6310 . . . . . . . 8 ..^
280228, 245, 2793eqtrd 2512 . . . . . . 7 ..^
281195, 280mpteq12dva 4530 . . . . . 6 ..^
282116, 172, 2813eqtrd 2512 . . . . 5 ..^
283282, 183oveq12d 6313 . . . 4 ..^ lim lim
284113, 283eleq12d 2549 . . 3 ..^ lim lim
285109, 284mpbird 232 . 2 ..^ lim
286 eqid 2467 . . . . 5
287 eqid 2467 . . . . 5
288 eqid 2467 . . . . 5
28927adantr 465 . . . . . . . . . 10
290251adantl 466 . . . . . . . . . . 11
291260, 290readdcld 9635 . . . . . . . . . 10
292289, 291ffvelrnd 6033 . . . . . . . . 9
29352, 292sseldi 3507 . . . . . . . 8
294293adantlr 714 . . . . . . 7 ..^
2952943adantl3 1154 . . . . . 6 ..^
296 limccl 22147 . . . . . . . . . . 11 lim
297296sseli 3505 . . . . . . . . . 10 lim
29835, 297syl 16 . . . . . . . . 9
299 fourierdlem75.w . . . . . . . . . 10
30052, 299sseldi 3507 . . . . . . . . 9
301298, 300ifcld 3988 . . . . . . . 8
302301adantr 465 . . . . . . 7
3033023ad2antl1 1158 . . . . . 6 ..^
304295, 303subcld 9942 . . . . 5 ..^
305251recnd 9634 . . . . . . 7
306305adantl 466 . . . . . 6 ..^
307225neqned 2670 . . . . . . . . 9 ..^
308307neneqd 2669 . . . . . . . 8 ..^
309 elsn 4047 . . . . . . . 8
310308, 309sylnibr 305 . . . . . . 7 ..^
3113103adantl3 1154 . . . . . 6 ..^
312306, 311eldifd 3492 . . . . 5 ..^
313 eqid 2467 . . . . . . . . . 10
314 eqid 2467 . . . . . . . . . 10
315 eqid 2467 . . . . . . . . . 10
316300ad2antrr 725 . . . . . . . . . 10 ..^
317 ioossre 11598 . . . . . . . . . . . 12
318317a1i 11 . . . . . . . . . . 11 ..^
319173adantl 466 . . . . . . . . . . . . . . 15 ..^
320319, 139syldan 470 . . . . . . . . . . . . . 14 ..^
321320rexrd 9655 . . . . . . . . . . . . 13 ..^
322321adantr 465 . . . . . . . . . . . 12 ..^
323291adantlr 714 . . . . . . . . . . . 12 ..^
324 iccssre 11618 . . . . . . . . . . . . . . . . . . . 20
325120, 119, 324mp2an 672 . . . . . . . . . . . . . . . . . . 19
326325, 52sstri 3518 . . . . . . . . . . . . . . . . . 18
327326a1i 11 . . . . . . . . . . . . . . . . 17 ..^
328176, 163eqeltrd 2555 . . . . . . . . . . . . . . . . . 18
3294, 319, 328syl2anc 661 . . . . . . . . . . . . . . . . 17 ..^
330327, 329sseldd 3510 . . . . . . . . . . . . . . . 16 ..^
331266, 330addcomd 9793 . . . . . . . . . . . . . . 15 ..^
332319, 141syldan 470 . . . . . . . . . . . . . . . . 17 ..^
333164fvmpt2 5964 . . . . . . . . . . . . . . . . 17
334319, 332, 333syl2anc 661 . . . . . . . . . . . . . . . 16 ..^
335334oveq1d 6310 . . . . . . . . . . . . . . 15 ..^
33652, 320sseldi 3507 . . . . . . . . . . . . . . . 16 ..^
337336, 266npcand 9946 . . . . . . . . . . . . . . 15 ..^
338331, 335, 3373eqtrrd 2513 . . . . . . . . . . . . . 14 ..^
339338adantr 465 . . . . . . . . . . . . 13 ..^
340334, 332eqeltrd 2555 . . . . . . . . . . . . . . 15 ..^
341340adantr 465 . . . . . . . . . . . . . 14 ..^
342239adantl 466 . . . . . . . . . . . . . 14 ..^
343341, 256, 261, 342ltadd2dd 9752 . . . . . . . . . . . . 13 ..^
344339, 343eqbrtrd 4473 . . . . . . . . . . . 12 ..^
345322, 248, 323, 344, 272eliood 31418 . . . . . . . . . . 11 ..^
346 ioossre 11598 . . . . . . . . . . . 12
347346a1i 11 . . . . . . . . . . 11 ..^
348341, 342gtned 9731 . . . . . . . . . . 11 ..^
349 fourierdlem75.r . . . . . . . . . . . 12 ..^ lim
350338oveq2d 6311 . . . . . . . . . . . 12 ..^ lim lim
351349, 350eleqtrd 2557 . . . . . . . . . . 11 ..^ lim
35228, 2, 318, 313, 345, 347, 348, 351, 330fourierdlem53 31783 . . . . . . . . . 10 ..^ lim
353 ioosscn 31414 . . . . . . . . . . . 12
354353a1i 11 . . . . . . . . . . 11 ..^
3554, 300syl 16 . . . . . . . . . . 11 ..^
356314, 354, 355, 330constlimc 31489 . . . . . . . . . 10 ..^ lim
357313, 314, 315, 294, 316, 352, 356sublimc 31517 . . . . . . . . 9 ..^ lim
358357adantr 465 . . . . . . . 8 ..^ lim
359 iftrue 3951 . . . . . . . . . . 11
360359oveq2d 6311 . . . . . . . . . 10
361360adantl 466 . . . . . . . . 9 ..^
362251adantl 466 . . . . . . . . . . . . . . 15 ..^
363 0re 9608 . . . . . . . . . . . . . . . 16
364363a1i 11 . . . . . . . . . . . . . . 15 ..^
365259adantlr 714 . . . . . . . . . . . . . . . 16 ..^
366262adantl 466 . . . . . . . . . . . . . . . 16 ..^
367193adantr 465 . . . . . . . . . . . . . . . . . 18 ..^
368321ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 ..^
36940ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 ..^
3702adantr 465 . . . . . . . . . . . . . . . . . . . . . 22 ..^
371370adantr 465 . . . . . . . . . . . . . . . . . . . . 21 ..^
372 simplr 754 . . . . . . . . . . . . . . . . . . . . 21 ..^
373 simpr 461 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
3742adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
37517adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
376374, 375ltnled 9743 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
377373, 376mpbird 232 . . . . . . . . . . . . . . . . . . . . . 22 ..^
378377adantlr 714 . . . . . . . . . . . . . . . . . . . . 21 ..^
379368, 369, 371, 372, 378eliood 31418 . . . . . . . . . . . . . . . . . . . 20 ..^
3807, 6, 5, 205fourierdlem12 31742 . . . . . . . . . . . . . . . . . . . . . 22 ..^
381380