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

Theorem fourierdlem51 31781
 Description: is in the periodic partition, when the considered interval is centered at . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem51.a
fourierdlem51.b
fourierdlem51.alt0
fourierdlem51.bgt0
fourierdlem51.t
fourierdlem51.cfi
fourierdlem51.css
fourierdlem51.bc
fourierdlem51.e
fourierdlem51.x
fourierdlem51.exc
fourierdlem51.d
fourierdlem51.f
fourierdlem51.h
Assertion
Ref Expression
fourierdlem51
Distinct variable groups:   ,,,   ,,,   ,,,   ,   ,,   ,   ,   ,,,   ,,,   ,   ,,
Allowed substitution hints:   ()   ()   ()   ()   (,,)   ()   (,)   (,,)   (,,)   ()

Proof of Theorem fourierdlem51
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem51.a . . . . . . . 8
2 fourierdlem51.x . . . . . . . 8
31, 2readdcld 9635 . . . . . . 7
4 fourierdlem51.b . . . . . . . 8
54, 2readdcld 9635 . . . . . . 7
6 0red 9609 . . . . . . . . . 10
7 fourierdlem51.alt0 . . . . . . . . . 10
81, 6, 2, 7ltadd1dd 10175 . . . . . . . . 9
92recnd 9634 . . . . . . . . . 10
109addid2d 9792 . . . . . . . . 9
118, 10breqtrd 4477 . . . . . . . 8
123, 2, 11ltled 9744 . . . . . . 7
1310eqcomd 2475 . . . . . . . . 9
14 fourierdlem51.bgt0 . . . . . . . . . 10
156, 4, 2, 14ltadd1dd 10175 . . . . . . . . 9
1613, 15eqbrtrd 4473 . . . . . . . 8
172, 5, 16ltled 9744 . . . . . . 7
183, 5, 2, 12, 17eliccd 31425 . . . . . 6
194, 2resubcld 9999 . . . . . . . . 9
20 fourierdlem51.t . . . . . . . . . 10
214, 1resubcld 9999 . . . . . . . . . 10
2220, 21syl5eqel 2559 . . . . . . . . 9
231, 6, 4, 7, 14lttrd 9754 . . . . . . . . . . . 12
241, 4posdifd 10151 . . . . . . . . . . . 12
2523, 24mpbid 210 . . . . . . . . . . 11
2620eqcomi 2480 . . . . . . . . . . . 12
2726a1i 11 . . . . . . . . . . 11
2825, 27breqtrd 4477 . . . . . . . . . 10
296, 28gtned 9731 . . . . . . . . 9
3019, 22, 29redivcld 10384 . . . . . . . 8
3130flcld 11915 . . . . . . 7
32 fourierdlem51.e . . . . . . . . . . 11
3332a1i 11 . . . . . . . . . 10
34 id 22 . . . . . . . . . . . 12
35 oveq2 6303 . . . . . . . . . . . . . . 15
3635oveq1d 6310 . . . . . . . . . . . . . 14
3736fveq2d 5876 . . . . . . . . . . . . 13
3837oveq1d 6310 . . . . . . . . . . . 12
3934, 38oveq12d 6313 . . . . . . . . . . 11
4039adantl 466 . . . . . . . . . 10
4131zred 10978 . . . . . . . . . . . 12
4241, 22remulcld 9636 . . . . . . . . . . 11
432, 42readdcld 9635 . . . . . . . . . 10
4433, 40, 2, 43fvmptd 5962 . . . . . . . . 9
4544eqcomd 2475 . . . . . . . 8
46 fourierdlem51.exc . . . . . . . 8
4745, 46eqeltrd 2555 . . . . . . 7
48 oveq1 6302 . . . . . . . . . 10
4948oveq2d 6311 . . . . . . . . 9
5049eleq1d 2536 . . . . . . . 8
5150rspcev 3219 . . . . . . 7
5231, 47, 51syl2anc 661 . . . . . 6
5318, 52jca 532 . . . . 5
54 oveq1 6302 . . . . . . . 8
5554eleq1d 2536 . . . . . . 7
5655rexbidv 2978 . . . . . 6
5756elrab 3266 . . . . 5
5853, 57sylibr 212 . . . 4
59 elun2 3677 . . . 4
6058, 59syl 16 . . 3
61 fourierdlem51.d . . . 4
6261eqcomi 2480 . . 3
6360, 62syl6eleq 2565 . 2
64 prfi 7807 . . . . . . . 8
6564a1i 11 . . . . . . 7
66 snfi 7608 . . . . . . . . . 10
6766a1i 11 . . . . . . . . 9
68 fourierdlem51.cfi . . . . . . . . . 10
69 fvres 5886 . . . . . . . . . . . . . . . 16
7069adantl 466 . . . . . . . . . . . . . . 15
71 oveq1 6302 . . . . . . . . . . . . . . . . . . . . 21
7271eleq1d 2536 . . . . . . . . . . . . . . . . . . . 20
7372rexbidv 2978 . . . . . . . . . . . . . . . . . . 19
7473elrab 3266 . . . . . . . . . . . . . . . . . 18
7574simprbi 464 . . . . . . . . . . . . . . . . 17
7675adantl 466 . . . . . . . . . . . . . . . 16
77 nfv 1683 . . . . . . . . . . . . . . . . . 18
78 nfcv 2629 . . . . . . . . . . . . . . . . . . 19
79 nfre1 2928 . . . . . . . . . . . . . . . . . . . 20
80 nfcv 2629 . . . . . . . . . . . . . . . . . . . 20
8179, 80nfrab 3048 . . . . . . . . . . . . . . . . . . 19
8278, 81nfel 2642 . . . . . . . . . . . . . . . . . 18
8377, 82nfan 1875 . . . . . . . . . . . . . . . . 17
84 nfv 1683 . . . . . . . . . . . . . . . . 17
85 simpl 457 . . . . . . . . . . . . . . . . . 18
863rexrd 9655 . . . . . . . . . . . . . . . . . . . . 21
87 iocssre 11616 . . . . . . . . . . . . . . . . . . . . 21
8886, 5, 87syl2anc 661 . . . . . . . . . . . . . . . . . . . 20
8988adantr 465 . . . . . . . . . . . . . . . . . . 19
9074simplbi 460 . . . . . . . . . . . . . . . . . . . 20
9190adantl 466 . . . . . . . . . . . . . . . . . . 19
9289, 91sseldd 3510 . . . . . . . . . . . . . . . . . 18
93 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . 25
944adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9594, 93resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9622adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9729adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9895, 96, 97redivcld 10384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9998flcld 11915 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
10099zred 10978 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
101100, 96remulcld 9636 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10293, 101readdcld 9635 . . . . . . . . . . . . . . . . . . . . . . . . 25
10332fvmpt2 5964 . . . . . . . . . . . . . . . . . . . . . . . . 25
10493, 102, 103syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24
105104ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
106 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
10799ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
108106, 107jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
109 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1101rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1114rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1121, 4, 23ltled 9744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
113 lbicc2 11648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
114110, 111, 112, 113syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
115114adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
116109, 115eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
117116adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
118117adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
119108, 118jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . 26
120104eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
121 iocssicc 11624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
122121a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1231, 4, 23, 20, 32fourierdlem4 31734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
124123ffvelrnda 6032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
125122, 124sseldd 3510 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
126120, 125eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
127126ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
128110adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
12994rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
130 iocgtlb 31422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
131128, 129, 124, 130syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
132131ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
133 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
134133eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
135134adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
136135, 105breq12d 4466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
137132, 136mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
138 zre 10880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
139138adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
14022adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
141139, 140remulcld 9636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
142141adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
143106, 142syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
144101ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
14593adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
146106, 145syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
147143, 144, 146ltadd2d 9749 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
148137, 147mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
149138ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
150100ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
15122, 28elrpd 11266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
152151adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
153152ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
154149, 150, 153ltmul1d 11305 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
155148, 154mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . 26
156 fvex 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
157 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
158157anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
159158anbi1d 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
160 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
161160oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
162161eleq1d 2536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
163159, 162anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
164 breq2 4457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
165163, 164anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
166 eqeq1 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
167165, 166imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
168 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
169168anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
170169anbi1d 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
171 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
172171oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
173172eleq1d 2536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
174170, 173anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
175174anbi1d 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
176 breq1 4456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
177175, 176anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
178 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
179178eqeq2d 2481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
180177, 179imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
181 simp-6l 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
182181, 1syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
183181, 4syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
184181, 23syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
18593ad5antr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
186 simp-5r 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
187 simp-4r 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
188 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
189 simpllr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
190 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
191182, 183, 184, 20, 185, 186, 187, 188, 189, 190fourierdlem6 31736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
192180, 191chvarv 1983 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
193167, 192vtoclg 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
194156, 193ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26
195119, 127, 155, 194syl21anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . 25
196195oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . 24
197196oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . 23
198139recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
19922recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
200199adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
201198, 200adddirp1d 31386 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
202201oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . 26
203202adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25
204203adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
20593recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
206205adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
207142recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
208199adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
209208adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
210206, 207, 209addassd 9630 . . . . . . . . . . . . . . . . . . . . . . . . . 26
211210eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . 25
212211adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
213 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . 26
214213adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . 25
2154recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2161recnd 9634 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
217215, 216, 199subaddd 9960 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
21827, 217mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . 26
219218ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . 25
220214, 219eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . 24
221204, 212, 2203eqtrd 2512 . . . . . . . . . . . . . . . . . . . . . . 23
222105, 197, 2213eqtrd 2512 . . . . . . . . . . . . . . . . . . . . . 22
223 fourierdlem51.bc . . . . . . . . . . . . . . . . . . . . . . 23
224223ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22
225222, 224eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . 21
2262253adantl3 1154 . . . . . . . . . . . . . . . . . . . 20
227 simpl1 999 . . . . . . . . . . . . . . . . . . . . . 22
228 simpl2 1000 . . . . . . . . . . . . . . . . . . . . . 22
229 fourierdlem51.css . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
230229sselda 3509 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
231230adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26
2322313adant2 1015 . . . . . . . . . . . . . . . . . . . . . . . . 25
233232adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
234 neqne 31339 . . . . . . . . . . . . . . . . . . . . . . . . 25
235234adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24
236233, 235jca 532 . . . . . . . . . . . . . . . . . . . . . . 23
2371adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
238227, 237syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
239227, 94syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
240145, 142readdcld 9635 . . . . . . . . . . . . . . . . . . . . . . . . . 26
241240rexrd 9655 . . . . . . . . . . . . . . . . . . . . . . . . 25
242227, 228, 241syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24
243238, 239, 242eliccelioc 31448 . . . . . . . . . . . . . . . . . . . . . . 23
244236, 243mpbird 232 . . . . . . . . . . . . . . . . . . . . . 22
245104ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
246237ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
24794ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
24823ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . 26
249145adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
25099ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
251 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . 26
252120, 124eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
253252ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
254 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26
255246, 247, 248, 20, 249, 250, 251, 253, 254fourierdlem35 31765 . . . . . . . . . . . . . . . . . . . . . . . . 25
256255oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . 24
257256oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . 23
258245, 257eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . 22
259227, 228, 244, 258syl21anc 1227 . . . . . . . . . . . . . . . . . . . . 21
260 simp3 998 . . . . . . . . . . . . . . . . . . . . . 22
261260adantr 465 . . . . . . . . . . . . . . . . . . . . 21
262259, 261eqeltrd 2555 . . . . . . . . . . . . . . . . . . . 20
263226, 262pm2.61dan 789 . . . . . . . . . . . . . . . . . . 19
2642633exp 1195 . . . . . . . . . . . . . . . . . 18
26585, 92, 264syl2anc 661 . . . . . . . . . . . . . . . . 17
26683, 84, 265rexlimd 2951 . . . . . . . . . . . . . . . 16
26776, 266mpd 15 . . . . . . . . . . . . . . 15
26870, 267eqeltrd 2555 . . . . . . . . . . . . . 14
269 eqid 2467 . . . . . . . . . . . . . 14
270268, 269fmptd 6056 . . . . . . . . . . . . 13
271 iocssre 11616 . . . . . . . . . . . . . . . . . 18
272110, 4, 271syl2anc 661 . . . . . . . . . . . . . . . . 17
273123, 272fssd 5746 . . . . . . . . . . . . . . . 16
27490ssriv 3513 . . . . . . . . . . . . . . . . . 18
275274a1i 11 . . . . . . . . . . . . . . . . 17
276275, 88sstrd 3519 . . . . . . . . . . . . . . . 16
277273, 276fssresd 5758 . . . . . . . . . . . . . . 15
278277feqmptd 5927 . . . . . . . . . . . . . 14
279278feq1d 5723 . . . . . . . . . . . . 13
280270, 279mpbird 232 . . . . . . . . . . . 12
281 simplll 757 . . . . . . . . . . . . . . . . . . 19
282 id 22 . . . . . . . . . . . . . . . . . . . . . 22
283 fourierdlem51.h . . . . . . . . . . . . . . . . . . . . . . 23
284283eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . 22
285282, 284syl6eleq 2565 . . . . . . . . . . . . . . . . . . . . 21
286285adantl 466 . . . . . . . . . . . . . . . . . . . 20
287286ad2antrr 725 . . . . . . . . . . . . . . . . . . 19
288281, 287jca 532 . . . . . . . . . . . . . . . . . 18
289 id 22 . . . . . . . . . . . . . . . . . . . 20
290289, 284syl6eleq 2565 . . . . . . . . . . . . . . . . . . 19
291290ad2antlr 726 . . . . . . . . . . . . . . . . . 18
292288, 291jca 532 . . . . . . . . . . . . . . . . 17
293 fvres 5886 . . . . . . . . . . . . . . . . . . . 20
294293eqcomd 2475 . . . . . . . . . . . . . . . . . . 19
295294ad2antlr 726 . . . . . . . . . . . . . . . . . 18
296 id 22 . . . . . . . . . . . . . . . . . . . 20
297296eqcomd 2475 . . . . . . . . . . . . . . . . . . 19
298297adantl 466 . . . . . . . . . . . . . . . . . 18
299 fvres 5886 . . . . . . . . . . . . . . . . . . . 20
300299adantl 466 . . . . . . . . . . . . . . . . . . 19
301300ad2antrr 725 . . . . . . . . . . . . . . . . . 18
302295, 298, 3013eqtrd 2512 . . . . . . . . . . . . . . . . 17
303292, 302jca 532 . . . . . . . . . . . . . . . 16
3041ad3antrrr 729 . . . . . . . . . . . . . . . . . . 19
3054ad3antrrr 729 . . . . . . . . . . . . . . . . . . 19
30623ad3antrrr 729 . . . . . . . . . . . . . . . . . . 19
3072ad3antrrr 729 . . . . . . . . . . . . . . . . . . 19
308 simpllr 758 . . . . . . . . . . . . . . . . . . 19
309 simplr 754 . . . . . . . . . . . . . . . . . . 19
310 simpr 461 . . . . . . . . . . . . . . . . . . 19
311304, 305, 306, 307, 283, 20, 32, 308, 309, 310fourierdlem19 31749 . . . . . . . . . . . . . . . . . 18
312310eqcomd 2475 . . . . . . . . . . . . . . . . . . 19
313304, 305, 306, 307, 283, 20, 32, 309, 308, 312fourierdlem19 31749 . . . . . . . . . . . . . . . . . 18
314311, 313jca 532 . . . . . . . . . . . . . . . . 17
315283, 276syl5eqss 3553 . . . . . . . . . . . . . . . . . . . . 21
316315adantr 465 . . . . . . . . . . . . . . . . . . . 20
317 simpr 461 . . . . . . . . . . . . . . . . . . . 20
318316, 317sseldd 3510 . . . . . . . . . . . . . . . . . . 19
319318ad2antrr 725 . . . . . . . . . . . . . . . . . 18
320316sselda 3509 . . . . . . . . . . . . . . . . . . 19
321320adantr 465 . . . . . . . . . . . . . . . . . 18
322319, 321lttri3d 9736 . . . . . . . . . . . . . . . . 17
323314, 322mpbird 232 . . . . . . . . . . . . . . . 16
324303, 323syl 16 . . . . . . . . . . . . . . 15
325324ex 434 . . . . . . . . . . . . . 14
326325ralrimiva 2881 . . . . . . . . . . . . 13
327326ralrimiva 2881 . . . . . . . . . . . 12
328280, 327jca 532 . . . . . . . . . . 11