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

Theorem fourierdlem75 38157
 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 . . . . 5
21ad2antrr 740 . . . 4 ..^
3 fourierdlem75.v . . . . . . . . . 10
4 fourierdlem75.m . . . . . . . . . . 11
5 fourierdlem75.p . . . . . . . . . . . 12 ..^
65fourierdlem2 38083 . . . . . . . . . . 11 ..^
74, 6syl 17 . . . . . . . . . 10 ..^
83, 7mpbid 215 . . . . . . . . 9 ..^
98simpld 466 . . . . . . . 8
10 elmapi 7511 . . . . . . . 8
119, 10syl 17 . . . . . . 7
1211adantr 472 . . . . . 6 ..^
13 fzofzp1 12037 . . . . . . 7 ..^
1413adantl 473 . . . . . 6 ..^
1512, 14ffvelrnd 6038 . . . . 5 ..^
1615adantr 472 . . . 4 ..^
17 eqcom 2478 . . . . . . 7
1817biimpi 199 . . . . . 6
1918adantl 473 . . . . 5 ..^
208simprrd 775 . . . . . . 7 ..^
2120r19.21bi 2776 . . . . . 6 ..^
2221adantr 472 . . . . 5 ..^
2319, 22eqbrtrd 4416 . . . 4 ..^
24 fourierdlem75.f . . . . . . 7
2524adantr 472 . . . . . 6 ..^
26 ioossre 11721 . . . . . . 7
2726a1i 11 . . . . . 6 ..^
2825, 27fssresd 5762 . . . . 5 ..^
2928adantr 472 . . . 4 ..^
30 limcresi 22919 . . . . . . . 8 lim lim
31 fourierdlem75.y . . . . . . . 8 lim
3230, 31sseldi 3416 . . . . . . 7 lim
3332adantr 472 . . . . . 6 ..^ lim
34 pnfxr 11435 . . . . . . . . . 10
3534a1i 11 . . . . . . . . 9 ..^
3615rexrd 9708 . . . . . . . . . 10 ..^
3715ltpnfd 11446 . . . . . . . . . 10 ..^
3836, 35, 37xrltled 37574 . . . . . . . . 9 ..^
39 iooss2 11697 . . . . . . . . 9
4035, 38, 39syl2anc 673 . . . . . . . 8 ..^
4140resabs1d 5140 . . . . . . 7 ..^
4241oveq1d 6323 . . . . . 6 ..^ lim lim
4333, 42eleqtrd 2551 . . . . 5 ..^ lim
4443adantr 472 . . . 4 ..^ lim
45 eqid 2471 . . . 4
46 ax-resscn 9614 . . . . . . . . . . 11
4746a1i 11 . . . . . . . . . 10
4824, 47fssd 5750 . . . . . . . . . 10
49 ssid 3437 . . . . . . . . . . 11
5049a1i 11 . . . . . . . . . 10
5126a1i 11 . . . . . . . . . 10
52 eqid 2471 . . . . . . . . . . 11 fld fld
5352tgioo2 21899 . . . . . . . . . . 11 fldt
5452, 53dvres 22945 . . . . . . . . . 10
5547, 48, 50, 51, 54syl22anc 1293 . . . . . . . . 9
56 fourierdlem75.g . . . . . . . . . . 11
5756eqcomi 2480 . . . . . . . . . 10
58 ioontr 37707 . . . . . . . . . 10
5957, 58reseq12i 5109 . . . . . . . . 9
6055, 59syl6eq 2521 . . . . . . . 8
6160adantr 472 . . . . . . 7
6261dmeqd 5042 . . . . . 6
6362adantlr 729 . . . . 5 ..^
64 fourierdlem75.gcn . . . . . . . . 9 ..^
6564adantr 472 . . . . . . . 8 ..^
66 oveq1 6315 . . . . . . . . . . 11
6766reseq2d 5111 . . . . . . . . . 10
6867feq1d 5724 . . . . . . . . 9
6968adantl 473 . . . . . . . 8 ..^
7065, 69mpbid 215 . . . . . . 7 ..^
7166adantl 473 . . . . . . . 8 ..^
7271feq2d 5725 . . . . . . 7 ..^
7370, 72mpbid 215 . . . . . 6 ..^
74 fdm 5745 . . . . . 6
7573, 74syl 17 . . . . 5 ..^
7663, 75eqtrd 2505 . . . 4 ..^
77 limcresi 22919 . . . . . . . 8 lim lim
78 fourierdlem75.e . . . . . . . 8 lim
7977, 78sseldi 3416 . . . . . . 7 lim
8079adantr 472 . . . . . 6 ..^ lim
8140resabs1d 5140 . . . . . . . 8 ..^
8260adantr 472 . . . . . . . 8 ..^
8381, 82eqtr4d 2508 . . . . . . 7 ..^
8483oveq1d 6323 . . . . . 6 ..^ lim lim
8580, 84eleqtrd 2551 . . . . 5 ..^ lim
8685adantr 472 . . . 4 ..^ lim
87 eqid 2471 . . . 4
88 oveq2 6316 . . . . . . 7
8988fveq2d 5883 . . . . . 6
9089oveq1d 6323 . . . . 5
9190cbvmptv 4488 . . . 4
92 id 22 . . . . 5
9392cbvmptv 4488 . . . 4
942, 16, 23, 29, 44, 45, 76, 86, 87, 91, 93fourierdlem61 38143 . . 3 ..^ lim
95 fourierdlem75.a . . . . 5
96 iftrue 3878 . . . . 5
9795, 96syl5eq 2517 . . . 4
9897adantl 473 . . 3 ..^
99 fourierdlem75.h . . . . . . 7
10099reseq1i 5107 . . . . . 6
101100a1i 11 . . . . 5 ..^
102 ioossicc 11745 . . . . . . . 8
103 pire 23492 . . . . . . . . . . . 12
104103renegcli 9955 . . . . . . . . . . 11
105104rexri 9711 . . . . . . . . . 10
106105a1i 11 . . . . . . . . 9 ..^
107103rexri 9711 . . . . . . . . . 10
108107a1i 11 . . . . . . . . 9 ..^
109104a1i 11 . . . . . . . . . . . 12
110103a1i 11 . . . . . . . . . . . 12
111104a1i 11 . . . . . . . . . . . . . . . . 17
112111, 1readdcld 9688 . . . . . . . . . . . . . . . 16
113103a1i 11 . . . . . . . . . . . . . . . . 17
114113, 1readdcld 9688 . . . . . . . . . . . . . . . 16
115112, 114iccssred 37698 . . . . . . . . . . . . . . 15
116115adantr 472 . . . . . . . . . . . . . 14
1175, 4, 3fourierdlem15 38096 . . . . . . . . . . . . . . 15
118117ffvelrnda 6037 . . . . . . . . . . . . . 14
119116, 118sseldd 3419 . . . . . . . . . . . . 13
1201adantr 472 . . . . . . . . . . . . 13
121119, 120resubcld 10068 . . . . . . . . . . . 12
122111recnd 9687 . . . . . . . . . . . . . . . 16
1231recnd 9687 . . . . . . . . . . . . . . . 16
124122, 123pncand 10006 . . . . . . . . . . . . . . 15
125124eqcomd 2477 . . . . . . . . . . . . . 14
126125adantr 472 . . . . . . . . . . . . 13
127112adantr 472 . . . . . . . . . . . . . 14
128114adantr 472 . . . . . . . . . . . . . . . . 17
129 elicc2 11724 . . . . . . . . . . . . . . . . 17
130127, 128, 129syl2anc 673 . . . . . . . . . . . . . . . 16
131118, 130mpbid 215 . . . . . . . . . . . . . . 15
132131simp2d 1043 . . . . . . . . . . . . . 14
133127, 119, 120, 132lesub1dd 10250 . . . . . . . . . . . . 13
134126, 133eqbrtrd 4416 . . . . . . . . . . . 12
135131simp3d 1044 . . . . . . . . . . . . . 14
136119, 128, 120, 135lesub1dd 10250 . . . . . . . . . . . . 13
137110recnd 9687 . . . . . . . . . . . . . 14
138123adantr 472 . . . . . . . . . . . . . 14
139137, 138pncand 10006 . . . . . . . . . . . . 13
140136, 139breqtrd 4420 . . . . . . . . . . . 12
141109, 110, 121, 134, 140eliccd 37697 . . . . . . . . . . 11
142 fourierdlem75.q . . . . . . . . . . 11
143141, 142fmptd 6061 . . . . . . . . . 10
144143adantr 472 . . . . . . . . 9 ..^
145 simpr 468 . . . . . . . . 9 ..^ ..^
146106, 108, 144, 145fourierdlem8 38089 . . . . . . . 8 ..^
147102, 146syl5ss 3429 . . . . . . 7 ..^
148147resmptd 5162 . . . . . 6 ..^
149148adantr 472 . . . . 5 ..^
150 elfzofz 11962 . . . . . . . 8 ..^
151 simpr 468 . . . . . . . . . . 11
152142fvmpt2 5972 . . . . . . . . . . 11
153151, 141, 152syl2anc 673 . . . . . . . . . 10
154153adantr 472 . . . . . . . . 9
155 oveq1 6315 . . . . . . . . . 10
156155adantl 473 . . . . . . . . 9
157123ad2antrr 740 . . . . . . . . . 10
158157subidd 9993 . . . . . . . . 9
159154, 156, 1583eqtrd 2509 . . . . . . . 8
160150, 159sylanl2 663 . . . . . . 7 ..^
161 fveq2 5879 . . . . . . . . . . . . 13
162161oveq1d 6323 . . . . . . . . . . . 12
163162cbvmptv 4488 . . . . . . . . . . 11
164142, 163eqtri 2493 . . . . . . . . . 10
165164a1i 11 . . . . . . . . 9 ..^
166 fveq2 5879 . . . . . . . . . . 11
167166oveq1d 6323 . . . . . . . . . 10
168167adantl 473 . . . . . . . . 9 ..^
1691adantr 472 . . . . . . . . . 10 ..^
17015, 169resubcld 10068 . . . . . . . . 9 ..^
171165, 168, 14, 170fvmptd 5969 . . . . . . . 8 ..^
172171adantr 472 . . . . . . 7 ..^
173160, 172oveq12d 6326 . . . . . 6 ..^
174 simplr 770 . . . . . . . . . 10 ..^
175 fourierdlem75.o . . . . . . . . . . . . 13 ..^
1764adantr 472 . . . . . . . . . . . . 13
177111, 113, 1, 5, 175, 4, 3, 142fourierdlem14 38095 . . . . . . . . . . . . . 14
178177adantr 472 . . . . . . . . . . . . 13
179 simpr 468 . . . . . . . . . . . . . 14
180 fourierdlem75.x . . . . . . . . . . . . . . . . . 18
181 ffn 5739 . . . . . . . . . . . . . . . . . . 19
182 fvelrnb 5926 . . . . . . . . . . . . . . . . . . 19
183117, 181, 1823syl 18 . . . . . . . . . . . . . . . . . 18
184180, 183mpbid 215 . . . . . . . . . . . . . . . . 17
185159ex 441 . . . . . . . . . . . . . . . . . 18
186185reximdva 2858 . . . . . . . . . . . . . . . . 17
187184, 186mpd 15 . . . . . . . . . . . . . . . 16
188121, 142fmptd 6061 . . . . . . . . . . . . . . . . 17
189 ffn 5739 . . . . . . . . . . . . . . . . 17
190 fvelrnb 5926 . . . . . . . . . . . . . . . . 17
191188, 189, 1903syl 18 . . . . . . . . . . . . . . . 16
192187, 191mpbird 240 . . . . . . . . . . . . . . 15
193192adantr 472 . . . . . . . . . . . . . 14
194179, 193eqeltrd 2549 . . . . . . . . . . . . 13
195175, 176, 178, 194fourierdlem12 38093 . . . . . . . . . . . 12 ..^
196195an32s 821 . . . . . . . . . . 11 ..^
197196adantlr 729 . . . . . . . . . 10 ..^
198174, 197pm2.65da 586 . . . . . . . . 9 ..^
199198adantlr 729 . . . . . . . 8 ..^
200199iffalsed 3883 . . . . . . 7 ..^
201160eqcomd 2477 . . . . . . . . . . . 12 ..^
202201adantr 472 . . . . . . . . . . 11 ..^
203 elioo3g 11690 . . . . . . . . . . . . . 14
204203biimpi 199 . . . . . . . . . . . . 13
205204simprld 773 . . . . . . . . . . . 12
206205adantl 473 . . . . . . . . . . 11 ..^
207202, 206eqbrtrd 4416 . . . . . . . . . 10 ..^
208207iftrued 3880 . . . . . . . . 9 ..^
209208oveq2d 6324 . . . . . . . 8 ..^
210209oveq1d 6323 . . . . . . 7 ..^
2111rexrd 9708 . . . . . . . . . . . . 13
212211ad3antrrr 744 . . . . . . . . . . . 12 ..^
21336ad2antrr 740 . . . . . . . . . . . 12 ..^
214169ad2antrr 740 . . . . . . . . . . . . 13 ..^
215 elioore 11691 . . . . . . . . . . . . . 14
216215adantl 473 . . . . . . . . . . . . 13 ..^
217214, 216readdcld 9688 . . . . . . . . . . . 12 ..^
218216, 207elrpd 11361 . . . . . . . . . . . . 13 ..^
219214, 218ltaddrpd 11394 . . . . . . . . . . . 12 ..^
220215adantl 473 . . . . . . . . . . . . . . 15 ..^
221188adantr 472 . . . . . . . . . . . . . . . . 17 ..^
222221, 14ffvelrnd 6038 . . . . . . . . . . . . . . . 16 ..^
223222adantr 472 . . . . . . . . . . . . . . 15 ..^
2241ad2antrr 740 . . . . . . . . . . . . . . 15 ..^
225204simprrd 775 . . . . . . . . . . . . . . . 16
226225adantl 473 . . . . . . . . . . . . . . 15 ..^
227220, 223, 224, 226ltadd2dd 9811 . . . . . . . . . . . . . 14 ..^
228171oveq2d 6324 . . . . . . . . . . . . . . . 16 ..^
229123adantr 472 . . . . . . . . . . . . . . . . 17 ..^
23015recnd 9687 . . . . . . . . . . . . . . . . 17 ..^
231229, 230pncan3d 10008 . . . . . . . . . . . . . . . 16 ..^
232228, 231eqtrd 2505 . . . . . . . . . . . . . . 15 ..^
233232adantr 472 . . . . . . . . . . . . . 14 ..^
234227, 233breqtrd 4420 . . . . . . . . . . . . 13 ..^
235234adantlr 729 . . . . . . . . . . . 12 ..^
236212, 213, 217, 219, 235eliood 37691 . . . . . . . . . . 11 ..^
237 fvres 5893 . . . . . . . . . . 11
238236, 237syl 17 . . . . . . . . . 10 ..^
239238eqcomd 2477 . . . . . . . . 9 ..^
240239oveq1d 6323 . . . . . . . 8 ..^
241240oveq1d 6323 . . . . . . 7 ..^
242200, 210, 2413eqtrd 2509 . . . . . 6 ..^
243173, 242mpteq12dva 4473 . . . . 5 ..^
244101, 149, 2433eqtrd 2509 . . . 4 ..^
245244, 160oveq12d 6326 . . 3 ..^ lim lim
24694, 98, 2453eltr4d 2564 . 2 ..^ lim
247 eqid 2471 . . . . 5
248 eqid 2471 . . . . 5
249 eqid 2471 . . . . 5
25024adantr 472 . . . . . . . . . 10
2511adantr 472 . . . . . . . . . . 11
252215adantl 473 . . . . . . . . . . 11
253251, 252readdcld 9688 . . . . . . . . . 10
254250, 253ffvelrnd 6038 . . . . . . . . 9
255254recnd 9687 . . . . . . . 8
256255adantlr 729 . . . . . . 7 ..^
2572563adantl3 1188 . . . . . 6 ..^
258 limccl 22909 . . . . . . . . . 10 lim
259258, 31sseldi 3416 . . . . . . . . 9
260 fourierdlem75.w . . . . . . . . . 10
261260recnd 9687 . . . . . . . . 9
262259, 261ifcld 3915 . . . . . . . 8
263262adantr 472 . . . . . . 7
2642633ad2antl1 1192 . . . . . 6 ..^
265257, 264subcld 10005 . . . . 5 ..^
266215recnd 9687 . . . . . . 7
267266adantl 473 . . . . . 6 ..^
268 elsn 3973 . . . . . . . 8
269198, 268sylnibr 312 . . . . . . 7 ..^
2702693adantl3 1188 . . . . . 6 ..^
271267, 270eldifd 3401 . . . . 5 ..^
272 eqid 2471 . . . . . . . . . 10
273 eqid 2471 . . . . . . . . . 10
274 eqid 2471 . . . . . . . . . 10
275261ad2antrr 740 . . . . . . . . . 10 ..^
276 ioossre 11721 . . . . . . . . . . . 12
277276a1i 11 . . . . . . . . . . 11 ..^
278150, 119sylan2 482 . . . . . . . . . . . . . 14 ..^
279278rexrd 9708 . . . . . . . . . . . . 13 ..^
280279adantr 472 . . . . . . . . . . . 12 ..^
28136adantr 472 . . . . . . . . . . . 12 ..^
282253adantlr 729 . . . . . . . . . . . 12 ..^
283 iccssre 11741 . . . . . . . . . . . . . . . . . . 19
284104, 103, 283mp2an 686 . . . . . . . . . . . . . . . . . 18
285284, 46sstri 3427 . . . . . . . . . . . . . . . . 17
286153, 141eqeltrd 2549 . . . . . . . . . . . . . . . . . 18
287150, 286sylan2 482 . . . . . . . . . . . . . . . . 17 ..^
288285, 287sseldi 3416 . . . . . . . . . . . . . . . 16 ..^
289229, 288addcomd 9853 . . . . . . . . . . . . . . 15 ..^
290150adantl 473 . . . . . . . . . . . . . . . . 17 ..^
291150, 121sylan2 482 . . . . . . . . . . . . . . . . 17 ..^
292142fvmpt2 5972 . . . . . . . . . . . . . . . . 17
293290, 291, 292syl2anc 673 . . . . . . . . . . . . . . . 16 ..^
294293oveq1d 6323 . . . . . . . . . . . . . . 15 ..^
295278recnd 9687 . . . . . . . . . . . . . . . 16 ..^
296295, 229npcand 10009 . . . . . . . . . . . . . . 15 ..^
297289, 294, 2963eqtrrd 2510 . . . . . . . . . . . . . 14 ..^
298297adantr 472 . . . . . . . . . . . . 13 ..^
299293, 291eqeltrd 2549 . . . . . . . . . . . . . . 15 ..^
300299adantr 472 . . . . . . . . . . . . . 14 ..^
301205adantl 473 . . . . . . . . . . . . . 14 ..^
302300, 220, 224, 301ltadd2dd 9811 . . . . . . . . . . . . 13 ..^
303298, 302eqbrtrd 4416 . . . . . . . . . . . 12 ..^
304280, 281, 282, 303, 234eliood 37691 . . . . . . . . . . 11 ..^
305 ioossre 11721 . . . . . . . . . . . 12
306305a1i 11 . . . . . . . . . . 11 ..^
307300, 301gtned 9787 . . . . . . . . . . 11 ..^
308 fourierdlem75.r . . . . . . . . . . . 12 ..^ lim
309297oveq2d 6324 . . . . . . . . . . . 12 ..^ lim lim
310308, 309eleqtrd 2551 . . . . . . . . . . 11 ..^ lim
31125, 169, 277, 272, 304, 306, 307, 310, 288fourierdlem53 38135 . . . . . . . . . 10 ..^ lim
312 ioosscn 37687 . . . . . . . . . . . 12
313312a1i 11 . . . . . . . . . . 11 ..^
314261adantr 472 . . . . . . . . . . 11 ..^
315273, 313, 314, 288constlimc 37801 . . . . . . . . . 10 ..^ lim
316272, 273, 274, 256, 275, 311, 315sublimc 37830 . . . . . . . . 9 ..^ lim
317316adantr 472 . . . . . . . 8 ..^ lim
318 iftrue 3878 . . . . . . . . . 10
319318oveq2d 6324 . . . . . . . . 9
320319adantl 473 . . . . . . . 8 ..^
321215adantl 473 . . . . . . . . . . . . 13 ..^
322 0red 9662 . . . . . . . . . . . . 13 ..^
323222ad2antrr 740 . . . . . . . . . . . . . 14 ..^
324225adantl 473 . . . . . . . . . . . . . 14 ..^
325171adantr 472 . . . . . . . . . . . . . . . 16 ..^
326279ad2antrr 740 . . . . . . . . . . . . . . . . . . 19 ..^
32736ad2antrr 740 . . . . . . . . . . . . . . . . . . 19 ..^
328169ad2antrr 740 . . . . . . . . . . . . . . . . . . 19 ..^
329 simplr 770 . . . . . . . . . . . . . . . . . . 19 ..^
330 simpr 468 . . . . . . . . . . . . . . . . . . . . 21 ..^
3311ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . 22 ..^
33215adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ..^
333331, 332ltnled 9799 . . . . . . . . . . . . . . . . . . . . 21 ..^
334330, 333mpbird 240 . . . . . . . . . . . . . . . . . . . 20 ..^
335334adantlr 729 . . . . . . . . . . . . . . . . . . 19 ..^
336326, 327, 328, 329, 335eliood 37691 . . . . . . . . . . . . . . . . . 18 ..^
3375, 4, 3, 180fourierdlem12 38093 . . . . . . . . . . . . . . . . . . 19 ..^
338337ad2antrr 740 . . . . . . . . . . . . . . . . . 18 ..^
339336, 338condan 811 . . . . . . . . . . . . . . . . 17 ..^
34015adantr 472 . . . . . . . . . . . . . . . . . 18 ..^
3411ad2antrr 740 . . . . . . . . . . . . . . . . . 18 ..^
342340, 341suble0d 10225 . . . . . . . . . . . . . . . . 17 ..^
343339, 342mpbird 240 . . . . . . . . . . . . . . . 16 ..^
344325, 343eqbrtrd 4416 . . . . . . . . . . . . . . 15 ..^
345344adantr 472 . . . . . . . . . . . . . 14 ..^
346321, 323, 322, 324, 345ltletrd 9812 . . . . . . . . . . . . 13 ..^
347321, 322, 346ltnsymd 9801 . . . . . . . . . . . 12 ..^
348347iffalsed 3883 . . . . . . . . . . 11 ..^
349348oveq2d 6324 . . . . . . . . . 10 ..^
350349mpteq2dva 4482 . . . . . . . . 9 ..^
351350oveq1d 6323 . . . . . . . 8 ..^ lim lim
352317, 320, 3513eltr4d 2564 . . . . . . 7 ..^ lim
3533523adantl3 1188 . . . . . 6 ..^ lim
354 eqid 2471 . . . . . . . . . 10
355 eqid 2471 . . . . . . . . . 10
356259ad2antrr 740 . . . . . . . . . 10 ..^
357259adantr 472 . . . . . . . . . . 11 ..^
358354, 313, 357, 288constlimc 37801 . . . . . . . . . 10 ..^ lim
359272, 354, 355, 256, 356, 311, 358sublimc 37830 . . . . . . . . 9 ..^ lim
360359adantr 472 . . . . . . . 8 ..^ lim
361 iffalse 3881 . . . . . . . . . 10
362361oveq2d 6324 . . . . . . . . 9
363362adantl 473 . . . . . . . 8 ..^
364 0red 9662 . . . . . . . . . . . . 13 ..^
365299ad2antrr 740 . . . . . . . . . . . . 13 ..^
366215adantl 473 . . . . . . . . . . . . 13 ..^
3671ad2antrr 740 . . . . . . . . . . . . . . . . 17 ..^
368278adantr 472 . . . . . . . . . . . . . . . . 17 ..^
369 simpr 468 . . . . . . . . . . . . . . . . 17 ..^
370367, 368, 369nltled 9802 . . . . . . . . . . . . . . . 16 ..^
371368, 367subge0d 10224 . . . . . . . . . . . . . . . 16 ..^
372370, 371mpbird 240 . . . . . . . . . . . . . . 15 ..^
373293eqcomd 2477 . . . . . . . . . . . . . . . 16 ..^