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

Theorem fourierdlem74 38156
 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 11962 . . . . . 6 ..^
2 pire 23492 . . . . . . . . . . . 12
32renegcli 9955 . . . . . . . . . . 11
43a1i 11 . . . . . . . . . 10
5 fourierdlem74.xre . . . . . . . . . 10
64, 5readdcld 9688 . . . . . . . . 9
72a1i 11 . . . . . . . . . 10
87, 5readdcld 9688 . . . . . . . . 9
96, 8iccssred 37698 . . . . . . . 8
109adantr 472 . . . . . . 7
11 fourierdlem74.p . . . . . . . . 9 ..^
12 fourierdlem74.m . . . . . . . . 9
13 fourierdlem74.v . . . . . . . . 9
1411, 12, 13fourierdlem15 38096 . . . . . . . 8
1514ffvelrnda 6037 . . . . . . 7
1610, 15sseldd 3419 . . . . . 6
171, 16sylan2 482 . . . . 5 ..^
1817adantr 472 . . . 4 ..^
195ad2antrr 740 . . . 4 ..^
2011fourierdlem2 38083 . . . . . . . . . 10 ..^
2112, 20syl 17 . . . . . . . . 9 ..^
2213, 21mpbid 215 . . . . . . . 8 ..^
2322simprrd 775 . . . . . . 7 ..^
2423r19.21bi 2776 . . . . . 6 ..^
2524adantr 472 . . . . 5 ..^
26 eqcom 2478 . . . . . . 7
2726biimpi 199 . . . . . 6
2827adantl 473 . . . . 5 ..^
2925, 28breqtrrd 4422 . . . 4 ..^
30 fourierdlem74.f . . . . . 6
31 ioossre 11721 . . . . . . 7
3231a1i 11 . . . . . 6
3330, 32fssresd 5762 . . . . 5
3433ad2antrr 740 . . . 4 ..^
35 limcresi 22919 . . . . . . . 8 lim lim
36 fourierdlem74.w . . . . . . . 8 lim
3735, 36sseldi 3416 . . . . . . 7 lim
3837adantr 472 . . . . . 6 ..^ lim
39 mnfxr 11437 . . . . . . . . . 10
4039a1i 11 . . . . . . . . 9 ..^
4117rexrd 9708 . . . . . . . . . 10 ..^
4217mnfltd 11449 . . . . . . . . . 10 ..^
4340, 41, 42xrltled 37574 . . . . . . . . 9 ..^
44 iooss1 11696 . . . . . . . . 9
4540, 43, 44syl2anc 673 . . . . . . . 8 ..^
4645resabs1d 5140 . . . . . . 7 ..^
4746oveq1d 6323 . . . . . 6 ..^ lim lim
4838, 47eleqtrd 2551 . . . . 5 ..^ lim
4948adantr 472 . . . 4 ..^ lim
50 eqid 2471 . . . 4
51 ax-resscn 9614 . . . . . . . . . 10
5251a1i 11 . . . . . . . . 9
5330, 52fssd 5750 . . . . . . . . 9
54 ssid 3437 . . . . . . . . . 10
5554a1i 11 . . . . . . . . 9
56 eqid 2471 . . . . . . . . . 10 fld fld
5756tgioo2 21899 . . . . . . . . . 10 fldt
5856, 57dvres 22945 . . . . . . . . 9
5952, 53, 55, 32, 58syl22anc 1293 . . . . . . . 8
60 fourierdlem74.g . . . . . . . . . . 11
6160eqcomi 2480 . . . . . . . . . 10
62 ioontr 37707 . . . . . . . . . 10
6361, 62reseq12i 5109 . . . . . . . . 9
6463a1i 11 . . . . . . . 8
6559, 64eqtrd 2505 . . . . . . 7
6665dmeqd 5042 . . . . . 6
6766ad2antrr 740 . . . . 5 ..^
68 fourierdlem74.gcn . . . . . . . 8 ..^
6968adantr 472 . . . . . . 7 ..^
70 oveq2 6316 . . . . . . . . . 10
7170reseq2d 5111 . . . . . . . . 9
7271, 70feq12d 5727 . . . . . . . 8
7372adantl 473 . . . . . . 7 ..^
7469, 73mpbid 215 . . . . . 6 ..^
75 fdm 5745 . . . . . 6
7674, 75syl 17 . . . . 5 ..^
7767, 76eqtrd 2505 . . . 4 ..^
78 limcresi 22919 . . . . . . . 8 lim lim
7945resabs1d 5140 . . . . . . . . 9 ..^
8079oveq1d 6323 . . . . . . . 8 ..^ lim lim
8178, 80syl5sseq 3466 . . . . . . 7 ..^ lim lim
82 fourierdlem74.e . . . . . . . 8 lim
8382adantr 472 . . . . . . 7 ..^ lim
8481, 83sseldd 3419 . . . . . 6 ..^ lim
8559, 64eqtr2d 2506 . . . . . . . 8
8685oveq1d 6323 . . . . . . 7 lim lim
8786adantr 472 . . . . . 6 ..^ lim lim
8884, 87eleqtrd 2551 . . . . 5 ..^ lim
8988adantr 472 . . . 4 ..^ lim
90 eqid 2471 . . . 4
91 oveq2 6316 . . . . . . 7
9291fveq2d 5883 . . . . . 6
9392oveq1d 6323 . . . . 5
9493cbvmptv 4488 . . . 4
95 id 22 . . . . 5
9695cbvmptv 4488 . . . 4
9718, 19, 29, 34, 49, 50, 77, 89, 90, 94, 96fourierdlem60 38142 . . 3 ..^ lim
98 fourierdlem74.a . . . . 5
99 iftrue 3878 . . . . 5
10098, 99syl5eq 2517 . . . 4
101100adantl 473 . . 3 ..^
102 fourierdlem74.h . . . . . . 7
103102reseq1i 5107 . . . . . 6
104103a1i 11 . . . . 5 ..^
105 ioossicc 11745 . . . . . . . 8
1063rexri 9711 . . . . . . . . . 10
107106a1i 11 . . . . . . . . 9 ..^
1082rexri 9711 . . . . . . . . . 10
109108a1i 11 . . . . . . . . 9 ..^
1103a1i 11 . . . . . . . . . . . 12
1112a1i 11 . . . . . . . . . . . 12
1125adantr 472 . . . . . . . . . . . . 13
11316, 112resubcld 10068 . . . . . . . . . . . 12
1144recnd 9687 . . . . . . . . . . . . . . . 16
1155recnd 9687 . . . . . . . . . . . . . . . 16
116114, 115pncand 10006 . . . . . . . . . . . . . . 15
117116eqcomd 2477 . . . . . . . . . . . . . 14
118117adantr 472 . . . . . . . . . . . . 13
1196adantr 472 . . . . . . . . . . . . . 14
1208adantr 472 . . . . . . . . . . . . . . . . 17
121 elicc2 11724 . . . . . . . . . . . . . . . . 17
122119, 120, 121syl2anc 673 . . . . . . . . . . . . . . . 16
12315, 122mpbid 215 . . . . . . . . . . . . . . 15
124123simp2d 1043 . . . . . . . . . . . . . 14
125119, 16, 112, 124lesub1dd 10250 . . . . . . . . . . . . 13
126118, 125eqbrtrd 4416 . . . . . . . . . . . 12
127123simp3d 1044 . . . . . . . . . . . . . 14
12816, 120, 112, 127lesub1dd 10250 . . . . . . . . . . . . 13
129111recnd 9687 . . . . . . . . . . . . . 14
130115adantr 472 . . . . . . . . . . . . . 14
131129, 130pncand 10006 . . . . . . . . . . . . 13
132128, 131breqtrd 4420 . . . . . . . . . . . 12
133110, 111, 113, 126, 132eliccd 37697 . . . . . . . . . . 11
134 fourierdlem74.q . . . . . . . . . . 11
135133, 134fmptd 6061 . . . . . . . . . 10
136135adantr 472 . . . . . . . . 9 ..^
137 simpr 468 . . . . . . . . 9 ..^ ..^
138107, 109, 136, 137fourierdlem8 38089 . . . . . . . 8 ..^
139105, 138syl5ss 3429 . . . . . . 7 ..^
140139resmptd 5162 . . . . . 6 ..^
141140adantr 472 . . . . 5 ..^
1421adantl 473 . . . . . . . . 9 ..^
1431, 113sylan2 482 . . . . . . . . 9 ..^
144134fvmpt2 5972 . . . . . . . . 9
145142, 143, 144syl2anc 673 . . . . . . . 8 ..^
146145adantr 472 . . . . . . 7 ..^
147 fveq2 5879 . . . . . . . . . . . . . 14
148147oveq1d 6323 . . . . . . . . . . . . 13
149148cbvmptv 4488 . . . . . . . . . . . 12
150134, 149eqtri 2493 . . . . . . . . . . 11
151150a1i 11 . . . . . . . . . 10 ..^
152 fveq2 5879 . . . . . . . . . . . 12
153152oveq1d 6323 . . . . . . . . . . 11
154153adantl 473 . . . . . . . . . 10 ..^
155 fzofzp1 12037 . . . . . . . . . . 11 ..^
156155adantl 473 . . . . . . . . . 10 ..^
15722simpld 466 . . . . . . . . . . . . . 14
158 elmapi 7511 . . . . . . . . . . . . . 14
159157, 158syl 17 . . . . . . . . . . . . 13
160159adantr 472 . . . . . . . . . . . 12 ..^
161160, 156ffvelrnd 6038 . . . . . . . . . . 11 ..^
1625adantr 472 . . . . . . . . . . 11 ..^
163161, 162resubcld 10068 . . . . . . . . . 10 ..^
164151, 154, 156, 163fvmptd 5969 . . . . . . . . 9 ..^
165164adantr 472 . . . . . . . 8 ..^
166 oveq1 6315 . . . . . . . . 9
167166adantl 473 . . . . . . . 8 ..^
168115ad2antrr 740 . . . . . . . . . 10
169168subidd 9993 . . . . . . . . 9
1701, 169sylanl2 663 . . . . . . . 8 ..^
171165, 167, 1703eqtrd 2509 . . . . . . 7 ..^
172146, 171oveq12d 6326 . . . . . 6 ..^
173 simplr 770 . . . . . . . . . 10 ..^
174 fourierdlem74.o . . . . . . . . . . . . 13 ..^
17512adantr 472 . . . . . . . . . . . . 13
1764, 7, 5, 11, 174, 12, 13, 134fourierdlem14 38095 . . . . . . . . . . . . . 14
177176adantr 472 . . . . . . . . . . . . 13
178 simpr 468 . . . . . . . . . . . . . 14
179 fourierdlem74.x . . . . . . . . . . . . . . . . . 18
180 ffn 5739 . . . . . . . . . . . . . . . . . . 19
181 fvelrnb 5926 . . . . . . . . . . . . . . . . . . 19
18214, 180, 1813syl 18 . . . . . . . . . . . . . . . . . 18
183179, 182mpbid 215 . . . . . . . . . . . . . . . . 17
184 simpr 468 . . . . . . . . . . . . . . . . . . . . . 22
185134fvmpt2 5972 . . . . . . . . . . . . . . . . . . . . . 22
186184, 133, 185syl2anc 673 . . . . . . . . . . . . . . . . . . . . 21
187186adantr 472 . . . . . . . . . . . . . . . . . . . 20
188 oveq1 6315 . . . . . . . . . . . . . . . . . . . . 21
189188adantl 473 . . . . . . . . . . . . . . . . . . . 20
190115subidd 9993 . . . . . . . . . . . . . . . . . . . . 21
191190ad2antrr 740 . . . . . . . . . . . . . . . . . . . 20
192187, 189, 1913eqtrd 2509 . . . . . . . . . . . . . . . . . . 19
193192ex 441 . . . . . . . . . . . . . . . . . 18
194193reximdva 2858 . . . . . . . . . . . . . . . . 17
195183, 194mpd 15 . . . . . . . . . . . . . . . 16
196113, 134fmptd 6061 . . . . . . . . . . . . . . . . 17
197 ffn 5739 . . . . . . . . . . . . . . . . 17
198 fvelrnb 5926 . . . . . . . . . . . . . . . . 17
199196, 197, 1983syl 18 . . . . . . . . . . . . . . . 16
200195, 199mpbird 240 . . . . . . . . . . . . . . 15
201200adantr 472 . . . . . . . . . . . . . 14
202178, 201eqeltrd 2549 . . . . . . . . . . . . 13
203174, 175, 177, 202fourierdlem12 38093 . . . . . . . . . . . 12 ..^
204203an32s 821 . . . . . . . . . . 11 ..^
205204adantlr 729 . . . . . . . . . 10 ..^
206173, 205pm2.65da 586 . . . . . . . . 9 ..^
207206adantlr 729 . . . . . . . 8 ..^
208207iffalsed 3883 . . . . . . 7 ..^
209 elioore 11691 . . . . . . . . . . . 12
210209adantl 473 . . . . . . . . . . 11 ..^
211 0red 9662 . . . . . . . . . . 11 ..^
212 elioo3g 11690 . . . . . . . . . . . . . . 15
213212biimpi 199 . . . . . . . . . . . . . 14
214213simprrd 775 . . . . . . . . . . . . 13
215214adantl 473 . . . . . . . . . . . 12 ..^
216171adantr 472 . . . . . . . . . . . 12 ..^
217215, 216breqtrd 4420 . . . . . . . . . . 11 ..^
218210, 211, 217ltnsymd 9801 . . . . . . . . . 10 ..^
219218iffalsed 3883 . . . . . . . . 9 ..^
220219oveq2d 6324 . . . . . . . 8 ..^
221220oveq1d 6323 . . . . . . 7 ..^
22241ad2antrr 740 . . . . . . . . . . 11 ..^
2235rexrd 9708 . . . . . . . . . . . 12
224223ad3antrrr 744 . . . . . . . . . . 11 ..^
225162ad2antrr 740 . . . . . . . . . . . 12 ..^
226225, 210readdcld 9688 . . . . . . . . . . 11 ..^
227115adantr 472 . . . . . . . . . . . . . . . 16 ..^
228 iccssre 11741 . . . . . . . . . . . . . . . . . . 19
2293, 2, 228mp2an 686 . . . . . . . . . . . . . . . . . 18
230229, 51sstri 3427 . . . . . . . . . . . . . . . . 17
231186, 133eqeltrd 2549 . . . . . . . . . . . . . . . . . 18
2321, 231sylan2 482 . . . . . . . . . . . . . . . . 17 ..^
233230, 232sseldi 3416 . . . . . . . . . . . . . . . 16 ..^
234227, 233addcomd 9853 . . . . . . . . . . . . . . 15 ..^
235145oveq1d 6323 . . . . . . . . . . . . . . 15 ..^
23617recnd 9687 . . . . . . . . . . . . . . . 16 ..^
237236, 227npcand 10009 . . . . . . . . . . . . . . 15 ..^
238234, 235, 2373eqtrrd 2510 . . . . . . . . . . . . . 14 ..^
239238adantr 472 . . . . . . . . . . . . 13 ..^
240145, 143eqeltrd 2549 . . . . . . . . . . . . . . 15 ..^
241240adantr 472 . . . . . . . . . . . . . 14 ..^
242209adantl 473 . . . . . . . . . . . . . 14 ..^
2435ad2antrr 740 . . . . . . . . . . . . . 14 ..^
244213simprld 773 . . . . . . . . . . . . . . 15
245244adantl 473 . . . . . . . . . . . . . 14 ..^
246241, 242, 243, 245ltadd2dd 9811 . . . . . . . . . . . . 13 ..^
247239, 246eqbrtrd 4416 . . . . . . . . . . . 12 ..^
248247adantlr 729 . . . . . . . . . . 11 ..^
249 ltaddneg 9865 . . . . . . . . . . . . 13
250210, 225, 249syl2anc 673 . . . . . . . . . . . 12 ..^
251217, 250mpbid 215 . . . . . . . . . . 11 ..^
252222, 224, 226, 248, 251eliood 37691 . . . . . . . . . 10 ..^
253 fvres 5893 . . . . . . . . . . 11
254253eqcomd 2477 . . . . . . . . . 10
255252, 254syl 17 . . . . . . . . 9 ..^
256255oveq1d 6323 . . . . . . . 8 ..^
257256oveq1d 6323 . . . . . . 7 ..^
258208, 221, 2573eqtrd 2509 . . . . . 6 ..^
259172, 258mpteq12dva 4473 . . . . 5 ..^
260104, 141, 2593eqtrd 2509 . . . 4 ..^
261260, 171oveq12d 6326 . . 3 ..^ lim lim
26297, 101, 2613eltr4d 2564 . 2 ..^ lim
263 eqid 2471 . . . . 5
264 eqid 2471 . . . . 5
265 eqid 2471 . . . . 5
26630adantr 472 . . . . . . . . . 10
2675adantr 472 . . . . . . . . . . 11
268209adantl 473 . . . . . . . . . . 11
269267, 268readdcld 9688 . . . . . . . . . 10
270266, 269ffvelrnd 6038 . . . . . . . . 9
271270recnd 9687 . . . . . . . 8
272271adantlr 729 . . . . . . 7 ..^
2732723adantl3 1188 . . . . . 6 ..^
274 fourierdlem74.y . . . . . . . . . 10
275274recnd 9687 . . . . . . . . 9
276 limccl 22909 . . . . . . . . . 10 lim
277276, 36sseldi 3416 . . . . . . . . 9
278275, 277ifcld 3915 . . . . . . . 8
279278adantr 472 . . . . . . 7
2802793ad2antl1 1192 . . . . . 6 ..^
281273, 280subcld 10005 . . . . 5 ..^
282209recnd 9687 . . . . . . 7
283282adantl 473 . . . . . 6 ..^
284 elsn 3973 . . . . . . . 8
285206, 284sylnibr 312 . . . . . . 7 ..^
2862853adantl3 1188 . . . . . 6 ..^
287283, 286eldifd 3401 . . . . 5 ..^
288 eqid 2471 . . . . . . . . . 10
289 eqid 2471 . . . . . . . . . 10
290 eqid 2471 . . . . . . . . . 10
291277ad2antrr 740 . . . . . . . . . 10 ..^
29230adantr 472 . . . . . . . . . . 11 ..^
293 ioossre 11721 . . . . . . . . . . . 12
294293a1i 11 . . . . . . . . . . 11 ..^
29541adantr 472 . . . . . . . . . . . 12 ..^
296161rexrd 9708 . . . . . . . . . . . . 13 ..^
297296adantr 472 . . . . . . . . . . . 12 ..^
298269adantlr 729 . . . . . . . . . . . 12 ..^
299196adantr 472 . . . . . . . . . . . . . . . 16 ..^
300299, 156ffvelrnd 6038 . . . . . . . . . . . . . . 15 ..^
301300adantr 472 . . . . . . . . . . . . . 14 ..^
302214adantl 473 . . . . . . . . . . . . . 14 ..^
303242, 301, 243, 302ltadd2dd 9811 . . . . . . . . . . . . 13 ..^
304164oveq2d 6324 . . . . . . . . . . . . . . 15 ..^
305161recnd 9687 . . . . . . . . . . . . . . . 16 ..^
306227, 305pncan3d 10008 . . . . . . . . . . . . . . 15 ..^
307304, 306eqtrd 2505 . . . . . . . . . . . . . 14 ..^
308307adantr 472 . . . . . . . . . . . . 13 ..^
309303, 308breqtrd 4420 . . . . . . . . . . . 12 ..^
310295, 297, 298, 247, 309eliood 37691 . . . . . . . . . . 11 ..^
311 ioossre 11721 . . . . . . . . . . . 12
312311a1i 11 . . . . . . . . . . 11 ..^
313242, 302ltned 9788 . . . . . . . . . . 11 ..^
314 fourierdlem74.r . . . . . . . . . . . 12 ..^ lim
315307eqcomd 2477 . . . . . . . . . . . . 13 ..^
316315oveq2d 6324 . . . . . . . . . . . 12 ..^ lim lim
317314, 316eleqtrd 2551 . . . . . . . . . . 11 ..^ lim
318300recnd 9687 . . . . . . . . . . 11 ..^
319292, 162, 294, 288, 310, 312, 313, 317, 318fourierdlem53 38135 . . . . . . . . . 10 ..^ lim
320 ioosscn 37687 . . . . . . . . . . . 12
321320a1i 11 . . . . . . . . . . 11 ..^
322277adantr 472 . . . . . . . . . . 11 ..^
323289, 321, 322, 318constlimc 37801 . . . . . . . . . 10 ..^ lim
324288, 289, 290, 272, 291, 319, 323sublimc 37830 . . . . . . . . 9 ..^ lim
325324adantr 472 . . . . . . . 8 ..^ lim
326 iftrue 3878 . . . . . . . . . 10
327326oveq2d 6324 . . . . . . . . 9
328327adantl 473 . . . . . . . 8 ..^
329209adantl 473 . . . . . . . . . . . . 13 ..^
330 0red 9662 . . . . . . . . . . . . 13 ..^
331300ad2antrr 740 . . . . . . . . . . . . . 14 ..^
332214adantl 473 . . . . . . . . . . . . . 14 ..^
333164adantr 472 . . . . . . . . . . . . . . . 16 ..^
334161adantr 472 . . . . . . . . . . . . . . . . . 18 ..^
3355ad2antrr 740 . . . . . . . . . . . . . . . . . 18 ..^
336 simpr 468 . . . . . . . . . . . . . . . . . 18 ..^
337334, 335, 336ltled 9800 . . . . . . . . . . . . . . . . 17 ..^
338334, 335suble0d 10225 . . . . . . . . . . . . . . . . 17 ..^
339337, 338mpbird 240 . . . . . . . . . . . . . . . 16 ..^
340333, 339eqbrtrd 4416 . . . . . . . . . . . . . . 15 ..^
341340adantr 472 . . . . . . . . . . . . . 14 ..^
342329, 331, 330, 332, 341ltletrd 9812 . . . . . . . . . . . . 13 ..^
343329, 330, 342ltnsymd 9801 . . . . . . . . . . . 12 ..^
344343iffalsed 3883 . . . . . . . . . . 11 ..^
345344oveq2d 6324 . . . . . . . . . 10 ..^
346345mpteq2dva 4482 . . . . . . . . 9 ..^
347346oveq1d 6323 . . . . . . . 8 ..^ lim lim
348325, 328, 3473eltr4d 2564 . . . . . . 7 ..^ lim
3493483adantl3 1188 . . . . . 6 ..^ lim
350 simpl1 1033 . . . . . . 7 ..^
351 simpl2 1034 . . . . . . 7 ..^ ..^
3525ad2antrr 740 . . . . . . . . 9 ..^
3533523adantl3 1188 . . . . . . . 8 ..^
354161adantr 472 . . . . . . . . 9 ..^
3553543adantl3 1188 . . . . . . . 8 ..^
356 neqne 2651 . . . . . . . . . . 11
357356necomd 2698 . . . . . . . . . 10
358357adantr 472 . . . . . . . . 9
3593583ad2antl3 1194 . . . . . . . 8 ..^
360 simpr 468 . . . . . . . 8 ..^
361353, 355, 359, 360lttri5d 37605 . . . . . . 7 ..^
362 eqid 2471 . . . . . . . 8
363272adantlr 729 . . . . . . . 8 ..^
364278ad3antrrr 744 . . . . . . . 8 ..^
365319adantr 472 . . . . . . . 8 ..^ lim
366 eqid 2471 . . . . . . . . . . 11
367275adantr 472 . . . . . . . . . . 11 ..^
368366, 321, 367, 318constlimc 37801 . . . . . . . . . 10 ..^ lim
369368adantr 472 . . . . . . . . 9 ..^ lim
3705ad2antrr 740 . . . . . . . . . . 11 ..^
371161adantr 472 . . . . . . . . . . 11 ..^
372 simpr 468 . . . . . . . . . . 11 ..^
373370, 371, 372ltnsymd 9801 . . . . . . . . . 10 ..^
374373iffalsed 3883 . . . . . . . . 9 ..^
375 0red 9662 . . . . . . . . . . . . 13 ..^