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

Theorem fourierdlem111 38193
 Description: The fourier partial sum for is the sum of two integrals, with the same integrand involving and the Dirichlet Kernel , but on two opposite intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem111.a
fourierdlem111.b
fourierdlem111.s
fourierdlem111.d
fourierdlem111.p ..^
fourierdlem111.m
fourierdlem111.q
fourierdlem111.x
fourierdlem111.6
fourierdlem111.fper
fourierdlem111.g
fourierdlem111.fcn ..^
fourierdlem111.r ..^ lim
fourierdlem111.l ..^ lim
fourierdlem111.t
fourierdlem111.o ..^
fourierdlem111.14
Assertion
Ref Expression
fourierdlem111
Distinct variable groups:   ,,   ,   ,,,   ,,,,   ,,,,   ,,,,,   ,,   ,,,   ,,   ,   ,,,   ,,,   ,   ,,   ,,,   ,   ,,   ,   ,,   ,,,   ,,,   ,,,,   ,   ,,   ,   ,,,,   ,,   ,
Allowed substitution hints:   ()   (,,,,,)   (,,,,,,)   (,)   (,,,,,,,)   (,)   (,,,,)   (,,,,,,,)   (,,,,,)   (,)   (,,,,)   (,,,,)   ()   (,,,,,,,)   (,)

Proof of Theorem fourierdlem111
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq1 2537 . . . . . 6
21anbi2d 718 . . . . 5
3 fveq2 5879 . . . . . 6
4 fveq2 5879 . . . . . . . . . 10
54fveq1d 5881 . . . . . . . . 9
65oveq2d 6324 . . . . . . . 8
76adantr 472 . . . . . . 7
87itgeq2dv 22818 . . . . . 6
93, 8eqeq12d 2486 . . . . 5
102, 9imbi12d 327 . . . 4
11 fourierdlem111.6 . . . . . 6
1211adantr 472 . . . . 5
13 eqid 2471 . . . . 5
14 ioossre 11721 . . . . . . . . 9
1514a1i 11 . . . . . . . 8
1611, 15feqresmpt 5933 . . . . . . 7
17 ioossicc 11745 . . . . . . . . 9
1817a1i 11 . . . . . . . 8
19 ioombl 22597 . . . . . . . . 9
2019a1i 11 . . . . . . . 8
2111adantr 472 . . . . . . . . 9
22 pire 23492 . . . . . . . . . . . . . . 15
2322renegcli 9955 . . . . . . . . . . . . . 14
2423, 22elicc2i 11725 . . . . . . . . . . . . 13
2524simp1bi 1045 . . . . . . . . . . . 12
2625ssriv 3422 . . . . . . . . . . 11
2726a1i 11 . . . . . . . . . 10
2827sselda 3418 . . . . . . . . 9
2921, 28ffvelrnd 6038 . . . . . . . 8
3011, 27feqresmpt 5933 . . . . . . . . 9
31 fourierdlem111.p . . . . . . . . . 10 ..^
32 fourierdlem111.m . . . . . . . . . 10
33 fourierdlem111.q . . . . . . . . . 10
34 ax-resscn 9614 . . . . . . . . . . . . 13
3534a1i 11 . . . . . . . . . . . 12
3611, 35fssd 5750 . . . . . . . . . . 11
3736, 27fssresd 5762 . . . . . . . . . 10
38 ioossicc 11745 . . . . . . . . . . . . 13
3923rexri 9711 . . . . . . . . . . . . . . 15
4039a1i 11 . . . . . . . . . . . . . 14 ..^
4122rexri 9711 . . . . . . . . . . . . . . 15
4241a1i 11 . . . . . . . . . . . . . 14 ..^
4331, 32, 33fourierdlem15 38096 . . . . . . . . . . . . . . 15
4443adantr 472 . . . . . . . . . . . . . 14 ..^
45 simpr 468 . . . . . . . . . . . . . 14 ..^ ..^
4640, 42, 44, 45fourierdlem8 38089 . . . . . . . . . . . . 13 ..^
4738, 46syl5ss 3429 . . . . . . . . . . . 12 ..^
4847resabs1d 5140 . . . . . . . . . . 11 ..^
49 fourierdlem111.fcn . . . . . . . . . . 11 ..^
5048, 49eqeltrd 2549 . . . . . . . . . 10 ..^
51 fourierdlem111.r . . . . . . . . . . 11 ..^ lim
5248oveq1d 6323 . . . . . . . . . . 11 ..^ lim lim
5351, 52eleqtrrd 2552 . . . . . . . . . 10 ..^ lim
54 fourierdlem111.l . . . . . . . . . . 11 ..^ lim
5548oveq1d 6323 . . . . . . . . . . 11 ..^ lim lim
5654, 55eleqtrrd 2552 . . . . . . . . . 10 ..^ lim
5731, 32, 33, 37, 50, 53, 56fourierdlem69 38151 . . . . . . . . 9
5830, 57eqeltrrd 2550 . . . . . . . 8
5918, 20, 29, 58iblss 22841 . . . . . . 7
6016, 59eqeltrd 2549 . . . . . 6
6160adantr 472 . . . . 5
62 fourierdlem111.a . . . . 5
63 fourierdlem111.b . . . . 5
64 fourierdlem111.x . . . . . 6
6564adantr 472 . . . . 5
66 fourierdlem111.s . . . . 5
67 fourierdlem111.d . . . . 5
68 simpr 468 . . . . 5
6912, 13, 61, 62, 63, 65, 66, 67, 68fourierdlem83 38165 . . . 4
7010, 69chvarv 2120 . . 3
7123a1i 11 . . . . 5
7222a1i 11 . . . . 5
7336adantr 472 . . . . . . . 8
7425adantl 473 . . . . . . . 8
7573, 74ffvelrnd 6038 . . . . . . 7
7675adantlr 729 . . . . . 6
7767dirkerf 38071 . . . . . . . . 9
7877ad2antlr 741 . . . . . . . 8
7964adantr 472 . . . . . . . . . 10
8074, 79resubcld 10068 . . . . . . . . 9
8180adantlr 729 . . . . . . . 8
8278, 81ffvelrnd 6038 . . . . . . 7
8382recnd 9687 . . . . . 6
8476, 83mulcld 9681 . . . . 5
8571, 72, 84itgioo 22852 . . . 4
86 fvres 5893 . . . . . . . 8
8786eqcomd 2477 . . . . . . 7
8887oveq1d 6323 . . . . . 6
8988adantl 473 . . . . 5
9089itgeq2dv 22818 . . . 4
91 simpl 464 . . . . . . . . . . . . 13
9291oveq2d 6324 . . . . . . . . . . . 12
9392oveq1d 6323 . . . . . . . . . . 11
9493oveq1d 6323 . . . . . . . . . 10
9591oveq1d 6323 . . . . . . . . . . . . 13
9695oveq1d 6323 . . . . . . . . . . . 12
9796fveq2d 5883 . . . . . . . . . . 11
9897oveq1d 6323 . . . . . . . . . 10
9994, 98ifeq12d 3892 . . . . . . . . 9
10099mpteq2dva 4482 . . . . . . . 8
101100cbvmptv 4488 . . . . . . 7
10267, 101eqtri 2493 . . . . . 6
103 fveq2 5879 . . . . . . . 8
104 oveq1 6315 . . . . . . . . 9
105104fveq2d 5883 . . . . . . . 8
106103, 105oveq12d 6326 . . . . . . 7
107106cbvmptv 4488 . . . . . 6
10833adantr 472 . . . . . 6
10932adantr 472 . . . . . 6
110 simpr 468 . . . . . 6
11164adantr 472 . . . . . 6
11237adantr 472 . . . . . 6
11350adantlr 729 . . . . . 6 ..^
11453adantlr 729 . . . . . 6 ..^ lim
11556adantlr 729 . . . . . 6 ..^ lim
116102, 31, 107, 108, 109, 110, 111, 112, 113, 114, 115fourierdlem101 38183 . . . . 5
117 oveq2 6316 . . . . . . . . . 10
118117fveq2d 5883 . . . . . . . . 9
119 fveq2 5879 . . . . . . . . 9
120118, 119oveq12d 6326 . . . . . . . 8
121120cbvitgv 22813 . . . . . . 7
122121a1i 11 . . . . . 6
12323a1i 11 . . . . . . . . 9
124123, 64resubcld 10068 . . . . . . . 8
125124adantr 472 . . . . . . 7
12622a1i 11 . . . . . . . . 9
127126, 64resubcld 10068 . . . . . . . 8
128127adantr 472 . . . . . . 7
12936adantr 472 . . . . . . . . . 10
13064adantr 472 . . . . . . . . . . 11
131 simpr 468 . . . . . . . . . . . . 13
132124adantr 472 . . . . . . . . . . . . . 14
133127adantr 472 . . . . . . . . . . . . . 14
134 elicc2 11724 . . . . . . . . . . . . . 14
135132, 133, 134syl2anc 673 . . . . . . . . . . . . 13
136131, 135mpbid 215 . . . . . . . . . . . 12
137136simp1d 1042 . . . . . . . . . . 11
138130, 137readdcld 9688 . . . . . . . . . 10
139129, 138ffvelrnd 6038 . . . . . . . . 9
140139adantlr 729 . . . . . . . 8
14177ad2antlr 741 . . . . . . . . . 10
142137adantlr 729 . . . . . . . . . 10
143141, 142ffvelrnd 6038 . . . . . . . . 9
144143recnd 9687 . . . . . . . 8
145140, 144mulcld 9681 . . . . . . 7
146125, 128, 145itgioo 22852 . . . . . 6
14723a1i 11 . . . . . . . . . . . 12
14822a1i 11 . . . . . . . . . . . 12
14964recnd 9687 . . . . . . . . . . . . . . . 16
150126recnd 9687 . . . . . . . . . . . . . . . . 17
151150negcld 9992 . . . . . . . . . . . . . . . 16
152149, 151pncan3d 10008 . . . . . . . . . . . . . . 15
153152eqcomd 2477 . . . . . . . . . . . . . 14
154153adantr 472 . . . . . . . . . . . . 13
155136simp2d 1043 . . . . . . . . . . . . . 14
156132, 137, 130, 155leadd2dd 10249 . . . . . . . . . . . . 13
157154, 156eqbrtrd 4416 . . . . . . . . . . . 12
158136simp3d 1044 . . . . . . . . . . . . . 14
159137, 133, 130, 158leadd2dd 10249 . . . . . . . . . . . . 13
160149adantr 472 . . . . . . . . . . . . . 14
161150adantr 472 . . . . . . . . . . . . . 14
162160, 161pncan3d 10008 . . . . . . . . . . . . 13
163159, 162breqtrd 4420 . . . . . . . . . . . 12
164147, 148, 138, 157, 163eliccd 37697 . . . . . . . . . . 11
165 fvres 5893 . . . . . . . . . . 11
166164, 165syl 17 . . . . . . . . . 10
167166eqcomd 2477 . . . . . . . . 9
168167adantlr 729 . . . . . . . 8
169168oveq1d 6323 . . . . . . 7
170169itgeq2dv 22818 . . . . . 6
171122, 146, 1703eqtrrd 2510 . . . . 5
172116, 171eqtrd 2505 . . . 4
17385, 90, 1723eqtrd 2509 . . 3
174 elioore 11691 . . . . . . . . 9
175174adantl 473 . . . . . . . 8
17636adantr 472 . . . . . . . . . . 11
17764adantr 472 . . . . . . . . . . . 12
178174adantl 473 . . . . . . . . . . . 12
179177, 178readdcld 9688 . . . . . . . . . . 11
180176, 179ffvelrnd 6038 . . . . . . . . . 10
181180adantlr 729 . . . . . . . . 9
18277ad2antlr 741 . . . . . . . . . . 11
183182, 175ffvelrnd 6038 . . . . . . . . . 10
184183recnd 9687 . . . . . . . . 9
185181, 184mulcld 9681 . . . . . . . 8
186 fourierdlem111.g . . . . . . . . . 10
187 oveq2 6316 . . . . . . . . . . . . 13
188187fveq2d 5883 . . . . . . . . . . . 12
189 fveq2 5879 . . . . . . . . . . . 12
190188, 189oveq12d 6326 . . . . . . . . . . 11
191190cbvmptv 4488 . . . . . . . . . 10
192186, 191eqtri 2493 . . . . . . . . 9
193192fvmpt2 5972 . . . . . . . 8
194175, 185, 193syl2anc 673 . . . . . . 7
195194eqcomd 2477 . . . . . 6
196195itgeq2dv 22818 . . . . 5
19736adantr 472 . . . . . . . . . . . . 13
19864adantr 472 . . . . . . . . . . . . . 14
199 simpr 468 . . . . . . . . . . . . . 14
200198, 199readdcld 9688 . . . . . . . . . . . . 13
201197, 200ffvelrnd 6038 . . . . . . . . . . . 12
202201adantlr 729 . . . . . . . . . . 11
20377adantl 473 . . . . . . . . . . . . 13
204203ffvelrnda 6037 . . . . . . . . . . . 12
205204recnd 9687 . . . . . . . . . . 11
206202, 205mulcld 9681 . . . . . . . . . 10
207206, 186fmptd 6061 . . . . . . . . 9
208207adantr 472 . . . . . . . 8
209124adantr 472 . . . . . . . . . 10
210127adantr 472 . . . . . . . . . 10
211 simpr 468 . . . . . . . . . 10
212 eliccre 37699 . . . . . . . . . 10
213209, 210, 211, 212syl3anc 1292 . . . . . . . . 9
214213adantlr 729 . . . . . . . 8
215208, 214ffvelrnd 6038 . . . . . . 7
216125, 128, 215itgioo 22852 . . . . . 6
217 fveq2 5879 . . . . . . 7
218217cbvitgv 22813 . . . . . 6
219216, 218syl6eq 2521 . . . . 5
220196, 219eqtrd 2505 . . . 4
221 eqid 2471 . . . . . . 7
222111renegcld 10067 . . . . . . 7
223 fourierdlem111.o . . . . . . 7 ..^
22431fourierdlem2 38083 . . . . . . . . . . . . . . . . . 18 ..^
22532, 224syl 17 . . . . . . . . . . . . . . . . 17 ..^
22633, 225mpbid 215 . . . . . . . . . . . . . . . 16 ..^
227226simpld 466 . . . . . . . . . . . . . . 15
228 elmapi 7511 . . . . . . . . . . . . . . 15
229227, 228syl 17 . . . . . . . . . . . . . 14
230229fnvinran 37398 . . . . . . . . . . . . 13
23164adantr 472 . . . . . . . . . . . . 13
232230, 231resubcld 10068 . . . . . . . . . . . 12
233 fourierdlem111.14 . . . . . . . . . . . 12
234232, 233fmptd 6061 . . . . . . . . . . 11
235 reex 9648 . . . . . . . . . . . . 13
236 ovex 6336 . . . . . . . . . . . . 13
237235, 236pm3.2i 462 . . . . . . . . . . . 12
238 elmapg 7503 . . . . . . . . . . . 12
239237, 238mp1i 13 . . . . . . . . . . 11
240234, 239mpbird 240 . . . . . . . . . 10
241233a1i 11 . . . . . . . . . . . 12
242 fveq2 5879 . . . . . . . . . . . . . 14
243226simprd 470 . . . . . . . . . . . . . . . 16 ..^
244243simpld 466 . . . . . . . . . . . . . . 15
245244simpld 466 . . . . . . . . . . . . . 14
246242, 245sylan9eqr 2527 . . . . . . . . . . . . 13
247246oveq1d 6323 . . . . . . . . . . . 12
248 0zd 10973 . . . . . . . . . . . . . 14
24932nnzd 11062 . . . . . . . . . . . . . 14
250 0red 9662 . . . . . . . . . . . . . . . 16
251 nnre 10638 . . . . . . . . . . . . . . . 16
252 nngt0 10660 . . . . . . . . . . . . . . . 16
253250, 251, 252ltled 9800 . . . . . . . . . . . . . . 15
25432, 253syl 17 . . . . . . . . . . . . . 14
255 eluz2 11188 . . . . . . . . . . . . . 14
256248, 249, 254, 255syl3anbrc 1214 . . . . . . . . . . . . 13
257 eluzfz1 11832 . . . . . . . . . . . . 13
258256, 257syl 17 . . . . . . . . . . . 12
259241, 247, 258, 124fvmptd 5969 . . . . . . . . . . 11
260 fveq2 5879 . . . . . . . . . . . . . 14
261244simprd 470 . . . . . . . . . . . . . 14
262260, 261sylan9eqr 2527 . . . . . . . . . . . . 13
263262oveq1d 6323 . . . . . . . . . . . 12
264 eluzfz2 11833 . . . . . . . . . . . . 13
265256, 264syl 17 . . . . . . . . . . . 12
266241, 263, 265, 127fvmptd 5969 . . . . . . . . . . 11
267259, 266jca 541 . . . . . . . . . 10
268229adantr 472 . . . . . . . . . . . . . 14 ..^
269 elfzofz 11962 . . . . . . . . . . . . . . 15 ..^
270269adantl 473 . . . . . . . . . . . . . 14 ..^
271268, 270ffvelrnd 6038 . . . . . . . . . . . . 13 ..^
272 fzofzp1 12037 . . . . . . . . . . . . . . 15 ..^
273272adantl 473 . . . . . . . . . . . . . 14 ..^
274268, 273ffvelrnd 6038 . . . . . . . . . . . . 13 ..^
27564adantr 472 . . . . . . . . . . . . 13 ..^
276243simprd 470 . . . . . . . . . . . . . 14 ..^
277276r19.21bi 2776 . . . . . . . . . . . . 13 ..^
278271, 274, 275, 277ltsub1dd 10246 . . . . . . . . . . . 12 ..^
279270, 232syldan 478 . . . . . . . . . . . . 13 ..^
280233fvmpt2 5972 . . . . . . . . . . . . 13
281270, 279, 280syl2anc 673 . . . . . . . . . . . 12 ..^
282 fveq2 5879 . . . . . . . . . . . . . . . . 17
283282oveq1d 6323 . . . . . . . . . . . . . . . 16
284283cbvmptv 4488 . . . . . . . . . . . . . . 15
285233, 284eqtri 2493 . . . . . . . . . . . . . 14
286285a1i 11 . . . . . . . . . . . . 13 ..^
287 fveq2 5879 . . . . . . . . . . . . . . 15
288287oveq1d 6323 . . . . . . . . . . . . . 14
289288adantl 473 . . . . . . . . . . . . 13 ..^
290274, 275resubcld 10068 . . . . . . . . . . . . 13 ..^
291286, 289, 273, 290fvmptd 5969 . . . . . . . . . . . 12 ..^
292278, 281, 2913brtr4d 4426 . . . . . . . . . . 11 ..^
293292ralrimiva 2809 . . . . . . . . . 10 ..^
294240, 267, 293jca32 544 . . . . . . . . 9 ..^
295223fourierdlem2 38083 . . . . . . . . . 10 ..^
29632, 295syl 17 . . . . . . . . 9 ..^
297294, 296mpbird 240 . . . . . . . 8
298297adantr 472 . . . . . . 7
299150, 151, 149nnncan2d 10040 . . . . . . . . . . . 12
300 picn 23493 . . . . . . . . . . . . . 14
3013002timesi 10753 . . . . . . . . . . . . 13
302 fourierdlem111.t . . . . . . . . . . . . 13
303300, 300subnegi 9973 . . . . . . . . . . . . 13
304301, 302, 3033eqtr4i 2503 . . . . . . . . . . . 12
305299, 304syl6eqr 2523 . . . . . . . . . . 11
306305oveq2d 6324 . . . . . . . . . 10
307306fveq2d 5883 . . . . . . . . 9
308307ad2antrr 740 . . . . . . . 8
309 simpr 468 . . . . . . . . . 10
310186fvmpt2 5972 . . . . . . . . . 10
311309, 206, 310syl2anc 673 . . . . . . . . 9
312149adantr 472 . . . . . . . . . . . . . . 15
313199recnd 9687 . . . . . . . . . . . . . . 15
314 2re 10701 . . . . . . . . . . . . . . . . . . . 20
315314, 22remulcli 9675 . . . . . . . . . . . . . . . . . . 19
316302, 315eqeltri 2545 . . . . . . . . . . . . . . . . . 18
317316a1i 11 . . . . . . . . . . . . . . . . 17
318317recnd 9687 . . . . . . . . . . . . . . . 16
319318adantr 472 . . . . . . . . . . . . . . 15
320312, 313, 319addassd 9683 . . . . . . . . . . . . . 14
321320eqcomd 2477 . . . . . . . . . . . . 13
322321fveq2d 5883 . . . . . . . . . . . 12
323 simpl 464 . . . . . . . . . . . . . 14
324323, 200jca 541 . . . . . . . . . . . . 13
325 eleq1 2537 . . . . . . . . . . . . . . . 16
326325anbi2d 718 . . . . . . . . . . . . . . 15
327 oveq1 6315 . . . . . . . . . . . . . . . . 17
328327fveq2d 5883 . . . . . . . . . . . . . . . 16
329 fveq2 5879 . . . . . . . . . . . . . . . 16
330328, 329eqeq12d 2486 . . . . . . . . . . . . . . 15
331326, 330imbi12d 327 . . . . . . . . . . . . . 14
332 eleq1 2537 . . . . . . . . . . . . . . . . 17
333332anbi2d 718 . . . . . . . . . . . . . . . 16
334 oveq1 6315 . . . . . . . . . . . . . . . . . 18
335334fveq2d 5883 . . . . . . . . . . . . . . . . 17
336 fveq2 5879 . . . . . . . . . . . . . . . . 17
337335, 336eqeq12d 2486 . . . . . . . . . . . . . . . 16
338333, 337imbi12d 327 . . . . . . . . . . . . . . 15
339 fourierdlem111.fper . . . . . . . . . . . . . . 15
340338, 339chvarv 2120 . . . . . . . . . . . . . 14
341331, 340vtoclg 3093 . . . . . . . . . . . . 13
342200, 324, 341sylc 61 . . . . . . . . . . . 12
343322, 342eqtr2d 2506 . . . . . . . . . . 11
344343adantlr 729 . . . . . . . . . 10
34567, 302dirkerper 38070 . . . . . . . . . . . 12
346345eqcomd 2477 . . . . . . . . . . 11
347346adantll 728 . . . . . . . . . 10
348344, 347oveq12d 6326 . . . . . . . . 9
349192a1i 11 . . . . . . . . . . 11
350 oveq2 6316 . . . . . . . . . . . . . 14
351350fveq2d 5883 . . . . . . . . . . . . 13
352 fveq2 5879 . . . . . . . . . . . . 13
353351, 352oveq12d 6326 . . . . . . . . . . . 12
354353adantl 473 . . . . . . . . . . 11
355316a1i 11 . . . . . . . . . . . 12
356309, 355readdcld 9688 . . . . . . . . . . 11
357316a1i 11 . . . . . . . . . . . . . . . 16
358199, 357readdcld 9688 . . . . . . . . . . . . . . 15
359198, 358readdcld 9688 . . . . . . . . . . . . . 14
360197, 359ffvelrnd 6038 . . . . . . . . . . . . 13
361360adantlr 729 . . . . . . . . . . . 12
36277ad2antlr 741 . . . . . . . . . . . . . 14
363362, 356ffvelrnd 6038 . . . . . . . . . . . . 13
364363recnd 9687 . . . . . . . . . . . 12
365361, 364mulcld 9681 . . . . . . . . . . 11
366349, 354, 356, 365fvmptd 5969 . . . . . . . . . 10
367366eqcomd 2477 . . . . . . . . 9
368311, 348, 3673eqtrrd 2510 . . . . . . . 8
369308, 368eqtrd 2505 . . . . . . 7
370192reseq1i 5107 . . . . . . . . . 10
371370a1i 11 . . . . . . . . 9 ..^
372 ioossre 11721 . . . . . . . . . 10
373 resmpt 5160 . . . . . . . . . 10
374372, 373ax-mp 5 . . . . . . . . 9
375371, 374syl6eq 2521 . . . . . . . 8 ..^
376271rexrd 9708 . . . . . . . . . . . . . 14 ..^
377376adantr 472 . . . . . . . . . . . . 13 ..^
378274rexrd 9708 . . . . . . . . . . . . . 14 ..^
379378adantr 472 . . . . . . . . . . . . 13 ..^
38064adantr 472 . . . . . . . . . . . . . . 15
381 elioore 11691 . . . . . . . . . . . . . . . 16
382381adantl 473 . . . . . . . . . . . . . . 15
383380, 382readdcld 9688 . . . . . . . . . . . . . 14
384383adantlr 729 . . . . . . . . . . . . 13 ..^
385 eleq1 2537 . . . . . . . . . . . . . . . 16
386385anbi2d 718 . . . . . . . . . . . . . . 15 ..^ ..^
387187breq2d 4407 . . . . . . . . . . . . . . 15
388386, 387imbi12d 327 . . . . . . . . . . . . . 14 ..^ ..^
389149adantr 472 . . . . . . . . . . . . . . . . . 18 ..^
390281, 279eqeltrd 2549 . . . . . . . . . . . . . . . . . . 19 ..^
391390recnd 9687 . . . . . . . . . . . . . . . . . 18 ..^
392389, 391addcomd 9853 . . . . . . . . . . . . . . . . 17 ..^
393281oveq1d 6323 . . . . . . . . . . . . . . . . 17 ..^
394271recnd 9687 . . . . . . . . . . . . . . . . . 18 ..^
395394, 389npcand 10009 . . . . . . . . . . . . . . . . 17 ..^
396392, 393, 3953eqtrrd 2510 . . . . . . . . . . . . . . . 16 ..^
397396adantr 472 . . . . . . . . . . . . . . 15 ..^
398390adantr 472 . . . . . . . . . . . . . . . 16 ..^
399 elioore 11691 . . . . . . . . . . . . . . . . 17
400399adantl 473 . . . . . . . . . . . . . . . 16 ..^
40164ad2antrr 740 . . . . . . . . . . . . . . . 16 ..^
402390rexrd 9708 . . . . . . . . . . . . . . . . . 18 ..^
403402adantr 472 . . . . . . . . . . . . . . . . 17 ..^
404291, 290eqeltrd 2549 . . . . . . . . . . . . . . . . . . 19 ..^
405404rexrd 9708 . . . . . . . . . . . . . . . . . 18 ..^
406405adantr 472 . . . . . . . . . . . . . . . . 17 ..^
407 simpr 468 . . . . . . . . . . . . . . . . 17 ..^
408 ioogtlb 37688 . . . . . . . . . . . . . . . . 17
409403, 406, 407, 408syl3anc 1292 . . . . . . . . . . . . . . . 16 ..^
410398, 400, 401, 409ltadd2dd 9811 . . . . . . . . . . . . . . 15 ..^
411397, 410eqbrtrd 4416 . . . . . . . . . . . . . 14 ..^
412388, 411chvarv 2120 . . . . . . . . . . . . 13 ..^
413187breq1d 4405 . . . . . . . . . . . . . . 15
414386, 413imbi12d 327 . . . . . . . . . . . . . 14 ..^ ..^
415404adantr 472 . . . . . . . . . . . . . . . 16 ..^
416 iooltub 37706 . . . . . . . . . . . . . . . . 17
417403, 406, 407, 416syl3anc 1292 . . . . . . . . . . . . . . . 16 ..^
418400, 415, 401, 417ltadd2dd 9811 . . . . . . . . . . . . . . 15 ..^