Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  lhop2 Unicode version

Theorem lhop2 19852
 Description: L'Hôpital's Rule for limits from the right. If and are differentiable real functions on , and and both approach 0 at , and and ' are not zero on , and the limit of ' ' at is , then the limit at also exists and equals . (Contributed by Mario Carneiro, 29-Dec-2016.)
Hypotheses
Ref Expression
lhop2.a
lhop2.b
lhop2.l
lhop2.f
lhop2.g
lhop2.if
lhop2.ig
lhop2.f0 lim
lhop2.g0 lim
lhop2.gn0
lhop2.gd0
lhop2.c lim
Assertion
Ref Expression
lhop2 lim
Distinct variable groups:   ,   ,   ,   ,   ,   ,

Proof of Theorem lhop2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 qssre 10540 . . 3
2 lhop2.a . . . 4
3 lhop2.b . . . . 5
43rexrd 9090 . . . 4
5 lhop2.l . . . 4
6 qbtwnxr 10742 . . . 4
72, 4, 5, 6syl3anc 1184 . . 3
8 ssrexv 3368 . . 3
91, 7, 8mpsyl 61 . 2
10 simpr 448 . . . . . 6
11 simprl 733 . . . . . . . 8
1211adantr 452 . . . . . . 7
133ad2antrr 707 . . . . . . 7
14 elioore 10902 . . . . . . . 8
1514adantl 453 . . . . . . 7
16 iooneg 10973 . . . . . . 7
1712, 13, 15, 16syl3anc 1184 . . . . . 6
1810, 17mpbid 202 . . . . 5
1918adantrr 698 . . . 4
20 lhop2.f . . . . . . . 8
2120ad2antrr 707 . . . . . . 7
22 elioore 10902 . . . . . . . . . . . . 13
2322adantl 453 . . . . . . . . . . . 12
2423recnd 9070 . . . . . . . . . . 11
2524negnegd 9358 . . . . . . . . . 10
26 simpr 448 . . . . . . . . . 10
2725, 26eqeltrd 2478 . . . . . . . . 9
2811adantr 452 . . . . . . . . . 10
293ad2antrr 707 . . . . . . . . . 10
3023renegcld 9420 . . . . . . . . . 10
31 iooneg 10973 . . . . . . . . . 10
3228, 29, 30, 31syl3anc 1184 . . . . . . . . 9
3327, 32mpbird 224 . . . . . . . 8
342adantr 452 . . . . . . . . . 10
35 simprrl 741 . . . . . . . . . . 11
3611rexrd 9090 . . . . . . . . . . . 12
37 xrltle 10698 . . . . . . . . . . . 12
3834, 36, 37syl2anc 643 . . . . . . . . . . 11
3935, 38mpd 15 . . . . . . . . . 10
40 iooss1 10907 . . . . . . . . . 10
4134, 39, 40syl2anc 643 . . . . . . . . 9
4241sselda 3308 . . . . . . . 8
4333, 42syldan 457 . . . . . . 7
4421, 43ffvelrnd 5830 . . . . . 6
4544recnd 9070 . . . . 5
46 lhop2.g . . . . . . . 8
4746ad2antrr 707 . . . . . . 7
4847, 43ffvelrnd 5830 . . . . . 6
4948recnd 9070 . . . . 5
50 lhop2.gn0 . . . . . . 7
5150ad2antrr 707 . . . . . 6
5246adantr 452 . . . . . . . . . . . 12
53 ax-resscn 9003 . . . . . . . . . . . 12
54 fss 5558 . . . . . . . . . . . 12
5552, 53, 54sylancl 644 . . . . . . . . . . 11
5655adantr 452 . . . . . . . . . 10
57 ffn 5550 . . . . . . . . . 10
5856, 57syl 16 . . . . . . . . 9
59 fnfvelrn 5826 . . . . . . . . 9
6058, 43, 59syl2anc 643 . . . . . . . 8
61 eleq1 2464 . . . . . . . 8
6260, 61syl5ibcom 212 . . . . . . 7
6362necon3bd 2604 . . . . . 6
6451, 63mpd 15 . . . . 5
6545, 49, 64divcld 9746 . . . 4
66 limcresi 19725 . . . . . 6 lim lim
67 ioossre 10928 . . . . . . . 8
68 resmpt 5150 . . . . . . . 8
6967, 68ax-mp 8 . . . . . . 7
7069oveq1i 6050 . . . . . 6 lim lim
7166, 70sseqtri 3340 . . . . 5 lim lim
72 eqid 2404 . . . . . . . 8
7372negcncf 18901 . . . . . . 7
7453, 73mp1i 12 . . . . . 6
753adantr 452 . . . . . 6
76 negeq 9254 . . . . . 6
7774, 75, 76cnmptlimc 19730 . . . . 5 lim
7871, 77sseldi 3306 . . . 4 lim
7975renegcld 9420 . . . . . 6
8011renegcld 9420 . . . . . . 7
8180rexrd 9090 . . . . . 6
82 simprrr 742 . . . . . . 7
8311, 75ltnegd 9560 . . . . . . 7
8482, 83mpbid 202 . . . . . 6
85 eqid 2404 . . . . . . 7
8644, 85fmptd 5852 . . . . . 6
87 eqid 2404 . . . . . . 7
8848, 87fmptd 5852 . . . . . 6
89 reex 9037 . . . . . . . . . . . 12
9089prid1 3872 . . . . . . . . . . 11
9190a1i 11 . . . . . . . . . 10
92 neg1cn 10023 . . . . . . . . . . 11
9392a1i 11 . . . . . . . . . 10
9420adantr 452 . . . . . . . . . . . 12
9594ffvelrnda 5829 . . . . . . . . . . 11
9695recnd 9070 . . . . . . . . . 10
97 fvex 5701 . . . . . . . . . . 11
9897a1i 11 . . . . . . . . . 10
99 ax-1cn 9004 . . . . . . . . . . . 12
10099a1i 11 . . . . . . . . . . 11
101 simpr 448 . . . . . . . . . . . . 13
102101recnd 9070 . . . . . . . . . . . 12
10399a1i 11 . . . . . . . . . . . 12
10491dvmptid 19796 . . . . . . . . . . . 12
105 ioossre 10928 . . . . . . . . . . . . 13
106105a1i 11 . . . . . . . . . . . 12
107 eqid 2404 . . . . . . . . . . . . 13 fld fld
108107tgioo2 18787 . . . . . . . . . . . 12 fldt
109 iooretop 18753 . . . . . . . . . . . . 13
110109a1i 11 . . . . . . . . . . . 12
11191, 102, 103, 104, 106, 108, 107, 110dvmptres 19802 . . . . . . . . . . 11
11291, 24, 100, 111dvmptneg 19805 . . . . . . . . . 10
11394feqmptd 5738 . . . . . . . . . . . 12
114113oveq2d 6056 . . . . . . . . . . 11
115 dvf 19747 . . . . . . . . . . . . 13
116 lhop2.if . . . . . . . . . . . . . . 15
117116adantr 452 . . . . . . . . . . . . . 14
118117feq2d 5540 . . . . . . . . . . . . 13
119115, 118mpbii 203 . . . . . . . . . . . 12
120119feqmptd 5738 . . . . . . . . . . 11
121114, 120eqtr3d 2438 . . . . . . . . . 10
122 fveq2 5687 . . . . . . . . . 10
123 fveq2 5687 . . . . . . . . . 10
12491, 91, 43, 93, 96, 98, 112, 121, 122, 123dvmptco 19811 . . . . . . . . 9
125119adantr 452 . . . . . . . . . . . . 13
126125, 43ffvelrnd 5830 . . . . . . . . . . . 12
127126, 93mulcomd 9065 . . . . . . . . . . 11
128126mulm1d 9441 . . . . . . . . . . 11
129127, 128eqtrd 2436 . . . . . . . . . 10
130129mpteq2dva 4255 . . . . . . . . 9
131124, 130eqtrd 2436 . . . . . . . 8
132131dmeqd 5031 . . . . . . 7
133 negex 9260 . . . . . . . 8
134 eqid 2404 . . . . . . . 8
135133, 134dmmpti 5533 . . . . . . 7
136132, 135syl6eq 2452 . . . . . 6
13752ffvelrnda 5829 . . . . . . . . . . 11
138137recnd 9070 . . . . . . . . . 10
139 fvex 5701 . . . . . . . . . . 11
140139a1i 11 . . . . . . . . . 10
14152feqmptd 5738 . . . . . . . . . . . 12
142141oveq2d 6056 . . . . . . . . . . 11
143 dvf 19747 . . . . . . . . . . . . 13
144 lhop2.ig . . . . . . . . . . . . . . 15
145144adantr 452 . . . . . . . . . . . . . 14
146145feq2d 5540 . . . . . . . . . . . . 13
147143, 146mpbii 203 . . . . . . . . . . . 12
148147feqmptd 5738 . . . . . . . . . . 11
149142, 148eqtr3d 2438 . . . . . . . . . 10
150 fveq2 5687 . . . . . . . . . 10
151 fveq2 5687 . . . . . . . . . 10
15291, 91, 43, 93, 138, 140, 112, 149, 150, 151dvmptco 19811 . . . . . . . . 9
153147adantr 452 . . . . . . . . . . . . 13
154153, 43ffvelrnd 5830 . . . . . . . . . . . 12
155154, 93mulcomd 9065 . . . . . . . . . . 11
156154mulm1d 9441 . . . . . . . . . . 11
157155, 156eqtrd 2436 . . . . . . . . . 10
158157mpteq2dva 4255 . . . . . . . . 9
159152, 158eqtrd 2436 . . . . . . . 8
160159dmeqd 5031 . . . . . . 7
161 negex 9260 . . . . . . . 8
162 eqid 2404 . . . . . . . 8
163161, 162dmmpti 5533 . . . . . . 7
164160, 163syl6eq 2452 . . . . . 6
16543adantrr 698 . . . . . . 7
166 limcresi 19725 . . . . . . . . 9 lim lim
167 resmpt 5150 . . . . . . . . . . 11
168105, 167ax-mp 8 . . . . . . . . . 10
169168oveq1i 6050 . . . . . . . . 9 lim lim
170166, 169sseqtri 3340 . . . . . . . 8 lim lim
17175recnd 9070 . . . . . . . . . 10
172171negnegd 9358 . . . . . . . . 9
173 eqid 2404 . . . . . . . . . . . 12
174173negcncf 18901 . . . . . . . . . . 11
17553, 174mp1i 12 . . . . . . . . . 10
176 negeq 9254 . . . . . . . . . 10
177175, 79, 176cnmptlimc 19730 . . . . . . . . 9 lim
178172, 177eqeltrrd 2479 . . . . . . . 8 lim
179170, 178sseldi 3306 . . . . . . 7 lim
180 lhop2.f0 . . . . . . . . 9 lim
181180adantr 452 . . . . . . . 8 lim
182113oveq1d 6055 . . . . . . . 8 lim lim
183181, 182eleqtrd 2480 . . . . . . 7 lim
184 eliooord 10926 . . . . . . . . . . . . . 14
185184adantl 453 . . . . . . . . . . . . 13
186185simpld 446 . . . . . . . . . . . 12
18729, 23, 186ltnegcon1d 9562 . . . . . . . . . . 11
18830, 187ltned 9165 . . . . . . . . . 10
189188neneqd 2583 . . . . . . . . 9
190189pm2.21d 100 . . . . . . . 8
191190impr 603 . . . . . . 7
192165, 96, 179, 183, 122, 191limcco 19733 . . . . . 6 lim
193 lhop2.g0 . . . . . . . . 9 lim
194193adantr 452 . . . . . . . 8 lim
195141oveq1d 6055 . . . . . . . 8 lim lim
196194, 195eleqtrd 2480 . . . . . . 7 lim
197189pm2.21d 100 . . . . . . . 8
198197impr 603 . . . . . . 7
199165, 138, 179, 196, 150, 198limcco 19733 . . . . . 6 lim
20060, 87fmptd 5852 . . . . . . . 8
201 frn 5556 . . . . . . . 8
202200, 201syl 16 . . . . . . 7
20350adantr 452 . . . . . . 7
204202, 203ssneldd 3311 . . . . . 6
205 lhop2.gd0 . . . . . . . 8
206205adantr 452 . . . . . . 7
207159rneqd 5056 . . . . . . . . 9
208207eleq2d 2471 . . . . . . . 8
209162, 161elrnmpti 5080 . . . . . . . . 9
210 eqcom 2406 . . . . . . . . . . 11
211154negeq0d 9359 . . . . . . . . . . . 12
212 ffn 5550 . . . . . . . . . . . . . . 15
213153, 212syl 16 . . . . . . . . . . . . . 14
214 fnfvelrn 5826 . . . . . . . . . . . . . 14
215213, 43, 214syl2anc 643 . . . . . . . . . . . . 13
216 eleq1 2464 . . . . . . . . . . . . 13
217215, 216syl5ibcom 212 . . . . . . . . . . . 12
218211, 217sylbird 227 . . . . . . . . . . 11
219210, 218syl5bi 209 . . . . . . . . . 10
220219rexlimdva 2790 . . . . . . . . 9
221209, 220syl5bi 209 . . . . . . . 8
222208, 221sylbid 207 . . . . . . 7
223206, 222mtod 170 . . . . . 6
224119ffvelrnda 5829 . . . . . . . . 9
225147ffvelrnda 5829 . . . . . . . . 9
226205ad2antrr 707 . . . . . . . . . 10
227147, 212syl 16 . . . . . . . . . . . . 13
228 fnfvelrn 5826 . . . . . . . . . . . . 13
229227, 228sylan 458 . . . . . . . . . . . 12
230 eleq1 2464 . . . . . . . . . . . 12
231229, 230syl5ibcom 212 . . . . . . . . . . 11
232231necon3bd 2604 . . . . . . . . . 10
233226, 232mpd 15 . . . . . . . . 9
234224, 225, 233divcld 9746 . . . . . . . 8
235 lhop2.c . . . . . . . . 9 lim
236235adantr 452 . . . . . . . 8 lim
237 fveq2 5687 . . . . . . . . 9
238 fveq2 5687 . . . . . . . . 9
239237, 238oveq12d 6058 . . . . . . . 8
240189pm2.21d 100 . . . . . . . . 9
241240impr 603 . . . . . . . 8
242165, 234, 179, 236, 239, 241limcco 19733 . . . . . . 7 lim
243 nfcv 2540 . . . . . . . . . . . . 13
244 nfcv 2540 . . . . . . . . . . . . 13
245 nfmpt1 4258 . . . . . . . . . . . . 13
246243, 244, 245nfov 6063 . . . . . . . . . . . 12
247 nfcv 2540 . . . . . . . . . . . 12
248246, 247nffv 5694 . . . . . . . . . . 11
249 nfcv 2540 . . . . . . . . . . 11
250 nfmpt1 4258 . . . . . . . . . . . . 13
251243, 244, 250nfov 6063 . . . . . . . . . . . 12
252251, 247nffv 5694 . . . . . . . . . . 11
253248, 249, 252nfov 6063 . . . . . . . . . 10
254 nfcv 2540 . . . . . . . . . 10
255 fveq2 5687 . . . . . . . . . . 11
256 fveq2 5687 . . . . . . . . . . 11
257255, 256oveq12d 6058 . . . . . . . . . 10
258253, 254, 257cbvmpt 4259 . . . . . . . . 9
259131fveq1d 5689 . . . . . . . . . . . . 13
260134fvmpt2 5771 . . . . . . . . . . . . . 14
261133, 260mpan2 653 . . . . . . . . . . . . 13
262259, 261sylan9eq 2456 . . . . . . . . . . . 12
263159fveq1d 5689 . . . . . . . . . . . . 13
264162fvmpt2 5771 . . . . . . . . . . . . . 14
265161, 264mpan2 653 . . . . . . . . . . . . 13
266263, 265sylan9eq 2456 . . . . . . . . . . . 12
267262, 266oveq12d 6058 . . . . . . . . . . 11
268205ad2antrr 707 . . . . . . . . . . . . 13
269217necon3bd 2604 . . . . . . . . . . . . 13
270268, 269mpd 15 . . . . . . . . . . . 12
271126, 154, 270div2negd 9761 . . . . . . . . . . 11
272267, 271eqtrd 2436 . . . . . . . . . 10
273272mpteq2dva 4255 . . . . . . . . 9
274258, 273syl5eq 2448 . . . . . . . 8
275274oveq1d 6055 . . . . . . 7 lim lim
276242, 275eleqtrrd 2481 . . . . . 6 lim
27779, 81, 84, 86, 88, 136, 164, 192, 199, 204, 223, 276lhop1 19851 . . . . 5 lim
278 nffvmpt1 5695 . . . . . . . . 9
279 nffvmpt1 5695 . . . . . . . . 9
280278, 249, 279nfov 6063 . . . . . . . 8
281 nfcv 2540 . . . . . . . 8
282 fveq2 5687 . . . . . . . . 9
283 fveq2 5687 . . . . . . . . 9
284282, 283oveq12d 6058 . . . . . . . 8
285280, 281, 284cbvmpt 4259 . . . . . . 7
286 fvex 5701 . . . . . . . . . 10
28785fvmpt2 5771 . . . . . . . . . 10
28826, 286, 287sylancl 644 . . . . . . . . 9
289 fvex 5701 . . . . . . . . . 10
29087fvmpt2 5771 . . . . . . . . . 10
29126, 289, 290sylancl 644 . . . . . . . . 9
292288, 291oveq12d 6058 . . . . . . . 8
293292mpteq2dva 4255 . . . . . . 7
294285, 293syl5eq 2448 . . . . . 6
295294oveq1d 6055 . . . . 5 lim lim
296277, 295eleqtrd 2480 . . . 4 lim
297 negeq 9254 . . . . . 6
298297fveq2d 5691 . . . . 5
299297fveq2d 5691 . . . . 5
300298, 299oveq12d 6058 . . . 4
30179adantr 452 . . . . . . . 8
302 eliooord 10926 . . . . . . . . . . 11
303302adantl 453 . . . . . . . . . 10
304303simprd 450 . . . . . . . . 9
30515, 13ltnegd 9560 . . . . . . . . 9
306304, 305mpbid 202 . . . . . . . 8
307301, 306gtned 9164 . . . . . . 7
308307neneqd 2583 . . . . . 6
309308pm2.21d 100 . . . . 5
310309impr 603 . . . 4
31119, 65, 78, 296, 300, 310limcco 19733 . . 3 lim
31215recnd 9070 . . . . . . . . 9
313312negnegd 9358 . . . . . . . 8
314313fveq2d 5691 . . . . . . 7
315313fveq2d 5691 . . . . . . 7
316314, 315oveq12d 6058 . . . . . 6
317316mpteq2dva 4255 . . . . 5
318317oveq1d 6055 . . . 4 lim lim
319 resmpt 5150 . . . . . 6
32041, 319syl 16 . . . . 5
321320oveq1d 6055 . . . 4 lim lim
322 fss 5558 . . . . . . . . 9
32394, 53, 322sylancl 644 . . . . . . . 8
324323ffvelrnda 5829 . . . . . . 7
32555ffvelrnda 5829 . . . . . . 7
32650ad2antrr 707 . . . . . . . 8
32755, 57syl 16 . . . . . . . . . . 11
328 fnfvelrn 5826 . . . . . . . . . . 11
329327, 328sylan 458 . . . . . . . . . 10
330 eleq1 2464 . . . . . . . . . 10
331329, 330syl5ibcom 212 . . . . . . . . 9
332331necon3bd 2604 . . . . . . . 8
333326, 332mpd 15 . . . . . . 7
334324, 325, 333divcld 9746 . . . . . 6
335 eqid 2404 . . . . . 6
336334, 335fmptd 5852 . . . . 5
337 ioossre 10928 . . . . . . 7
338337, 53sstri 3317 . . . . . 6
339338a1i 11 . . . . 5
340 eqid 2404 . . . . 5 fldt fldt
341 ssun2 3471 . . . . . . 7
342 snssg 3892 . . . . . . . 8
34375, 342syl 16 . . . . . . 7
344341, 343mpbiri 225 . . . . . 6
345107cnfldtopon 18770 . . . . . . . . 9 fld TopOn
346337a1i 11 . . . . . . . . . . 11
34775snssd 3903 . . . . . . . . . . 11
348346, 347unssd 3483 . . . . . . . . . 10
349348, 53syl6ss 3320 . . . . . . . . 9
350 resttopon 17179 . . . . . . . . 9 fld TopOn fldt TopOn
351345, 349, 350sylancr 645 . . . . . . . 8 fldt TopOn
352 topontop 16946 . . . . . . . 8 fldt TopOn fldt
353351, 352syl 16 . . . . . . 7 fldt
354 indi 3547 . . . . . . . . . 10
355 pnfxr 10669 . . . . . . . . . . . . . 14
356355a1i 11 . . . . . . . . . . . . 13
3574adantr 452 . . . . . . . . . . . . 13
358 iooin 10906 . . . . . . . . . . . . 13
35936, 356, 34, 357, 358syl22anc 1185 . . . . . . . . . . . 12
360 xrltnle 9100 . . . . . . . . . . . . . . . 16
36134, 36, 360syl2anc 643 . . . . . . . . . . . . . . 15
36235, 361mpbid 202 . . . . . . . . . . . . . 14
363 iffalse 3706 . . . . . . . . . . . . . 14
364362, 363syl 16 . . . . . . . . . . . . 13
365 ltpnf 10677 . . . . . . . . . . . . . . . 16
36675, 365syl 16 . . . . . . . . . . . . . . 15
367 xrltnle 9100 . . . . . . . . . . . . . . . 16
368357, 355, 367sylancl 644 . . . . . . . . . . . . . . 15