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

Theorem lhop 19853
 Description: L'Hôpital's Rule. If is an open set of the reals, and are real functions on containing all of except possibly , which are differentiable everywhere on , and both approach 0, and the limit of ' ' at is , then the limit at also exists and equals . (Contributed by Mario Carneiro, 30-Dec-2016.)
Hypotheses
Ref Expression
lhop.a
lhop.f
lhop.g
lhop.i
lhop.b
lhop.d
lhop.if
lhop.ig
lhop.f0 lim
lhop.g0 lim
lhop.gn0
lhop.gd0
lhop.c lim
Assertion
Ref Expression
lhop lim
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem lhop
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqid 2404 . . . . 5
21rexmet 18775 . . . 4
32a1i 11 . . 3
4 lhop.i . . 3
5 lhop.b . . 3
6 eqid 2404 . . . . 5
71, 6tgioo 18780 . . . 4
87mopni2 18476 . . 3
93, 4, 5, 8syl3anc 1184 . 2
10 elssuni 4003 . . . . . . . . 9
11 uniretop 18749 . . . . . . . . 9
1210, 11syl6sseqr 3355 . . . . . . . 8
134, 12syl 16 . . . . . . 7
1413, 5sseldd 3309 . . . . . 6
15 rpre 10574 . . . . . 6
161bl2ioo 18776 . . . . . 6
1714, 15, 16syl2an 464 . . . . 5
1817sseq1d 3335 . . . 4
1914adantr 452 . . . . . . . . . . 11
20 simprl 733 . . . . . . . . . . . 12
2120rpred 10604 . . . . . . . . . . 11
2219, 21resubcld 9421 . . . . . . . . . 10
2322rexrd 9090 . . . . . . . . 9
2419, 20ltsubrpd 10632 . . . . . . . . 9
25 lhop.f . . . . . . . . . . 11
2625adantr 452 . . . . . . . . . 10
27 ssun1 3470 . . . . . . . . . . . 12
28 unass 3464 . . . . . . . . . . . . . . 15
29 uncom 3451 . . . . . . . . . . . . . . . 16
3029uneq1i 3457 . . . . . . . . . . . . . . 15
3128, 30eqtr3i 2426 . . . . . . . . . . . . . 14
3219rexrd 9090 . . . . . . . . . . . . . . 15
3319, 21readdcld 9071 . . . . . . . . . . . . . . . 16
3433rexrd 9090 . . . . . . . . . . . . . . 15
3519, 20ltaddrpd 10633 . . . . . . . . . . . . . . 15
36 ioojoin 10983 . . . . . . . . . . . . . . 15
3723, 32, 34, 24, 35, 36syl32anc 1192 . . . . . . . . . . . . . 14
3831, 37syl5eq 2448 . . . . . . . . . . . . 13
39 elioo2 10913 . . . . . . . . . . . . . . . . 17
4023, 34, 39syl2anc 643 . . . . . . . . . . . . . . . 16
4119, 24, 35, 40mpbir3and 1137 . . . . . . . . . . . . . . 15
4241snssd 3903 . . . . . . . . . . . . . 14
43 incom 3493 . . . . . . . . . . . . . . 15
44 ubioo 10904 . . . . . . . . . . . . . . . . . 18
45 lbioo 10903 . . . . . . . . . . . . . . . . . 18
4644, 45pm3.2ni 828 . . . . . . . . . . . . . . . . 17
47 elun 3448 . . . . . . . . . . . . . . . . 17
4846, 47mtbir 291 . . . . . . . . . . . . . . . 16
49 disjsn 3828 . . . . . . . . . . . . . . . 16
5048, 49mpbir 201 . . . . . . . . . . . . . . 15
5143, 50eqtri 2424 . . . . . . . . . . . . . 14
52 uneqdifeq 3676 . . . . . . . . . . . . . 14
5342, 51, 52sylancl 644 . . . . . . . . . . . . 13
5438, 53mpbid 202 . . . . . . . . . . . 12
5527, 54syl5sseqr 3357 . . . . . . . . . . 11
56 ssdif 3442 . . . . . . . . . . . . . 14
5756ad2antll 710 . . . . . . . . . . . . 13
58 lhop.d . . . . . . . . . . . . 13
5957, 58syl6sseqr 3355 . . . . . . . . . . . 12
60 lhop.if . . . . . . . . . . . . . 14
61 ax-resscn 9003 . . . . . . . . . . . . . . . 16
6261a1i 11 . . . . . . . . . . . . . . 15
63 fss 5558 . . . . . . . . . . . . . . . 16
6425, 61, 63sylancl 644 . . . . . . . . . . . . . . 15
65 lhop.a . . . . . . . . . . . . . . 15
6662, 64, 65dvbss 19741 . . . . . . . . . . . . . 14
6760, 66sstrd 3318 . . . . . . . . . . . . 13
6867adantr 452 . . . . . . . . . . . 12
6959, 68sstrd 3318 . . . . . . . . . . 11
7055, 69sstrd 3318 . . . . . . . . . 10
71 fssres 5569 . . . . . . . . . 10
7226, 70, 71syl2anc 643 . . . . . . . . 9
73 lhop.g . . . . . . . . . . 11
7473adantr 452 . . . . . . . . . 10
75 fssres 5569 . . . . . . . . . 10
7674, 70, 75syl2anc 643 . . . . . . . . 9
7761a1i 11 . . . . . . . . . . . . 13
7864adantr 452 . . . . . . . . . . . . 13
7965adantr 452 . . . . . . . . . . . . 13
80 ioossre 10928 . . . . . . . . . . . . . 14
8180a1i 11 . . . . . . . . . . . . 13
82 eqid 2404 . . . . . . . . . . . . . 14 fld fld
8382tgioo2 18787 . . . . . . . . . . . . . 14 fldt
8482, 83dvres 19751 . . . . . . . . . . . . 13
8577, 78, 79, 81, 84syl22anc 1185 . . . . . . . . . . . 12
86 retop 18748 . . . . . . . . . . . . . 14
87 iooretop 18753 . . . . . . . . . . . . . 14
88 isopn3i 17101 . . . . . . . . . . . . . 14
8986, 87, 88mp2an 654 . . . . . . . . . . . . 13
9089reseq2i 5102 . . . . . . . . . . . 12
9185, 90syl6eq 2452 . . . . . . . . . . 11
9291dmeqd 5031 . . . . . . . . . 10
9355, 59sstrd 3318 . . . . . . . . . . . 12
9460adantr 452 . . . . . . . . . . . 12
9593, 94sstrd 3318 . . . . . . . . . . 11
96 ssdmres 5127 . . . . . . . . . . 11
9795, 96sylib 189 . . . . . . . . . 10
9892, 97eqtrd 2436 . . . . . . . . 9
99 fss 5558 . . . . . . . . . . . . . . 15
10073, 61, 99sylancl 644 . . . . . . . . . . . . . 14
101100adantr 452 . . . . . . . . . . . . 13
10282, 83dvres 19751 . . . . . . . . . . . . 13
10377, 101, 79, 81, 102syl22anc 1185 . . . . . . . . . . . 12
10489reseq2i 5102 . . . . . . . . . . . 12
105103, 104syl6eq 2452 . . . . . . . . . . 11
106105dmeqd 5031 . . . . . . . . . 10
107 lhop.ig . . . . . . . . . . . . 13
108107adantr 452 . . . . . . . . . . . 12
10993, 108sstrd 3318 . . . . . . . . . . 11
110 ssdmres 5127 . . . . . . . . . . 11
111109, 110sylib 189 . . . . . . . . . 10
112106, 111eqtrd 2436 . . . . . . . . 9
113 limcresi 19725 . . . . . . . . . 10 lim lim
114 lhop.f0 . . . . . . . . . . 11 lim
115114adantr 452 . . . . . . . . . 10 lim
116113, 115sseldi 3306 . . . . . . . . 9 lim
117 limcresi 19725 . . . . . . . . . 10 lim lim
118 lhop.g0 . . . . . . . . . . 11 lim
119118adantr 452 . . . . . . . . . 10 lim
120117, 119sseldi 3306 . . . . . . . . 9 lim
121 df-ima 4850 . . . . . . . . . . 11
122 imass2 5199 . . . . . . . . . . . 12
12393, 122syl 16 . . . . . . . . . . 11
124121, 123syl5eqssr 3353 . . . . . . . . . 10
125 lhop.gn0 . . . . . . . . . . 11
126125adantr 452 . . . . . . . . . 10
127124, 126ssneldd 3311 . . . . . . . . 9
128105rneqd 5056 . . . . . . . . . . . 12
129 df-ima 4850 . . . . . . . . . . . 12
130128, 129syl6eqr 2454 . . . . . . . . . . 11
131 imass2 5199 . . . . . . . . . . . 12
13293, 131syl 16 . . . . . . . . . . 11
133130, 132eqsstrd 3342 . . . . . . . . . 10
134 lhop.gd0 . . . . . . . . . . 11
135134adantr 452 . . . . . . . . . 10
136133, 135ssneldd 3311 . . . . . . . . 9
137 limcresi 19725 . . . . . . . . . . 11 lim lim
138 resmpt 5150 . . . . . . . . . . . . . 14
13993, 138syl 16 . . . . . . . . . . . . 13
14091fveq1d 5689 . . . . . . . . . . . . . . . 16
141 fvres 5704 . . . . . . . . . . . . . . . 16
142140, 141sylan9eq 2456 . . . . . . . . . . . . . . 15
143105fveq1d 5689 . . . . . . . . . . . . . . . 16
144 fvres 5704 . . . . . . . . . . . . . . . 16
145143, 144sylan9eq 2456 . . . . . . . . . . . . . . 15
146142, 145oveq12d 6058 . . . . . . . . . . . . . 14
147146mpteq2dva 4255 . . . . . . . . . . . . 13
148139, 147eqtr4d 2439 . . . . . . . . . . . 12
149148oveq1d 6055 . . . . . . . . . . 11 lim lim
150137, 149syl5sseq 3356 . . . . . . . . . 10 lim lim
151 lhop.c . . . . . . . . . . 11 lim
152151adantr 452 . . . . . . . . . 10 lim
153150, 152sseldd 3309 . . . . . . . . 9 lim
15423, 19, 24, 72, 76, 98, 112, 116, 120, 127, 136, 153lhop2 19852 . . . . . . . 8 lim
155 resmpt 5150 . . . . . . . . . . 11
15655, 155syl 16 . . . . . . . . . 10
157 fvres 5704 . . . . . . . . . . . 12
158 fvres 5704 . . . . . . . . . . . 12
159157, 158oveq12d 6058 . . . . . . . . . . 11
160159mpteq2ia 4251 . . . . . . . . . 10
161156, 160syl6eqr 2454 . . . . . . . . 9
162161oveq1d 6055 . . . . . . . 8 lim lim
163154, 162eleqtrrd 2481 . . . . . . 7 lim
164 ssun2 3471 . . . . . . . . . . . 12
165164, 54syl5sseqr 3357 . . . . . . . . . . 11
166165, 69sstrd 3318 . . . . . . . . . 10
167 fssres 5569 . . . . . . . . . 10
16826, 166, 167syl2anc 643 . . . . . . . . 9
169 fssres 5569 . . . . . . . . . 10
17074, 166, 169syl2anc 643 . . . . . . . . 9
171 ioossre 10928 . . . . . . . . . . . . . 14
172171a1i 11 . . . . . . . . . . . . 13
17382, 83dvres 19751 . . . . . . . . . . . . 13
17477, 78, 79, 172, 173syl22anc 1185 . . . . . . . . . . . 12
175 iooretop 18753 . . . . . . . . . . . . . 14
176 isopn3i 17101 . . . . . . . . . . . . . 14
17786, 175, 176mp2an 654 . . . . . . . . . . . . 13
178177reseq2i 5102 . . . . . . . . . . . 12
179174, 178syl6eq 2452 . . . . . . . . . . 11
180179dmeqd 5031 . . . . . . . . . 10
181165, 59sstrd 3318 . . . . . . . . . . . 12
182181, 94sstrd 3318 . . . . . . . . . . 11
183 ssdmres 5127 . . . . . . . . . . 11
184182, 183sylib 189 . . . . . . . . . 10
185180, 184eqtrd 2436 . . . . . . . . 9
18682, 83dvres 19751 . . . . . . . . . . . . 13
18777, 101, 79, 172, 186syl22anc 1185 . . . . . . . . . . . 12
188177reseq2i 5102 . . . . . . . . . . . 12
189187, 188syl6eq 2452 . . . . . . . . . . 11
190189dmeqd 5031 . . . . . . . . . 10
191181, 108sstrd 3318 . . . . . . . . . . 11
192 ssdmres 5127 . . . . . . . . . . 11
193191, 192sylib 189 . . . . . . . . . 10
194190, 193eqtrd 2436 . . . . . . . . 9
195 limcresi 19725 . . . . . . . . . 10 lim lim
196195, 115sseldi 3306 . . . . . . . . 9 lim
197 limcresi 19725 . . . . . . . . . 10 lim lim
198197, 119sseldi 3306 . . . . . . . . 9 lim
199 df-ima 4850 . . . . . . . . . . 11
200 imass2 5199 . . . . . . . . . . . 12
201181, 200syl 16 . . . . . . . . . . 11
202199, 201syl5eqssr 3353 . . . . . . . . . 10
203202, 126ssneldd 3311 . . . . . . . . 9
204189rneqd 5056 . . . . . . . . . . . 12
205 df-ima 4850 . . . . . . . . . . . 12
206204, 205syl6eqr 2454 . . . . . . . . . . 11
207 imass2 5199 . . . . . . . . . . . 12
208181, 207syl 16 . . . . . . . . . . 11
209206, 208eqsstrd 3342 . . . . . . . . . 10
210209, 135ssneldd 3311 . . . . . . . . 9
211 limcresi 19725 . . . . . . . . . . 11 lim lim
212 resmpt 5150 . . . . . . . . . . . . . 14
213181, 212syl 16 . . . . . . . . . . . . 13
214179fveq1d 5689 . . . . . . . . . . . . . . . 16
215 fvres 5704 . . . . . . . . . . . . . . . 16
216214, 215sylan9eq 2456 . . . . . . . . . . . . . . 15
217189fveq1d 5689 . . . . . . . . . . . . . . . 16
218 fvres 5704 . . . . . . . . . . . . . . . 16
219217, 218sylan9eq 2456 . . . . . . . . . . . . . . 15
220216, 219oveq12d 6058 . . . . . . . . . . . . . 14
221220mpteq2dva 4255 . . . . . . . . . . . . 13
222213, 221eqtr4d 2439 . . . . . . . . . . . 12
223222oveq1d 6055 . . . . . . . . . . 11 lim lim
224211, 223syl5sseq 3356 . . . . . . . . . 10 lim lim
225224, 152sseldd 3309 . . . . . . . . 9 lim
22619, 34, 35, 168, 170, 185, 194, 196, 198, 203, 210, 225lhop1 19851 . . . . . . . 8 lim
227 resmpt 5150 . . . . . . . . . . 11
228165, 227syl 16 . . . . . . . . . 10
229 fvres 5704 . . . . . . . . . . . 12
230 fvres 5704 . . . . . . . . . . . 12
231229, 230oveq12d 6058 . . . . . . . . . . 11
232231mpteq2ia 4251 . . . . . . . . . 10
233228, 232syl6eqr 2454 . . . . . . . . 9
234233oveq1d 6055 . . . . . . . 8 lim lim
235226, 234eleqtrrd 2481 . . . . . . 7 lim
236 elin 3490 . . . . . . 7 lim lim lim lim
237163, 235, 236sylanbrc 646 . . . . . 6 lim lim
238 resmpt 5150 . . . . . . . . 9
23959, 238syl 16 . . . . . . . 8
240239oveq1d 6055 . . . . . . 7 lim lim
24167sselda 3308 . . . . . . . . . . . . 13
24225ffvelrnda 5829 . . . . . . . . . . . . 13
243241, 242syldan 457 . . . . . . . . . . . 12
244243recnd 9070 . . . . . . . . . . 11
24573ffvelrnda 5829 . . . . . . . . . . . . 13
246241, 245syldan 457 . . . . . . . . . . . 12
247246recnd 9070 . . . . . . . . . . 11
248125adantr 452 . . . . . . . . . . . 12
249 ffn 5550 . . . . . . . . . . . . . . . . 17
25073, 249syl 16 . . . . . . . . . . . . . . . 16
251250adantr 452 . . . . . . . . . . . . . . 15
25267adantr 452 . . . . . . . . . . . . . . 15
253 simpr 448 . . . . . . . . . . . . . . 15
254 fnfvima 5935 . . . . . . . . . . . . . . 15
255251, 252, 253, 254syl3anc 1184 . . . . . . . . . . . . . 14
256 eleq1 2464 . . . . . . . . . . . . . 14
257255, 256syl5ibcom 212 . . . . . . . . . . . . 13
258257necon3bd 2604 . . . . . . . . . . . 12
259248, 258mpd 15 . . . . . . . . . . 11
260244, 247, 259divcld 9746 . . . . . . . . . 10
261260adantlr 696 . . . . . . . . 9
262 eqid 2404 . . . . . . . . 9
263261, 262fmptd 5852 . . . . . . . 8
264 difss 3434 . . . . . . . . . . 11
26558, 264eqsstri 3338 . . . . . . . . . 10
26613, 61syl6ss 3320 . . . . . . . . . 10
267265, 266syl5ss 3319 . . . . . . . . 9
268267adantr 452 . . . . . . . 8
269 eqid 2404 . . . . . . . 8 fldt fldt
27058uneq1i 3457 . . . . . . . . . . . . . . . . 17
271 undif1 3663 . . . . . . . . . . . . . . . . 17
272270, 271eqtri 2424 . . . . . . . . . . . . . . . 16
273 simprr 734 . . . . . . . . . . . . . . . . . 18
27442, 273sstrd 3318 . . . . . . . . . . . . . . . . 17
275 ssequn2 3480 . . . . . . . . . . . . . . . . 17
276274, 275sylib 189 . . . . . . . . . . . . . . . 16
277272, 276syl5eq 2448 . . . . . . . . . . . . . . 15
278277oveq2d 6056 . . . . . . . . . . . . . 14 fldt fldt
27913adantr 452 . . . . . . . . . . . . . . 15
280 eqid 2404 . . . . . . . . . . . . . . . 16
28182, 280rerest 18788 . . . . . . . . . . . . . . 15 fldt t
282279, 281syl 16 . . . . . . . . . . . . . 14 fldt t
283278, 282eqtrd 2436 . . . . . . . . . . . . 13 fldt t
284283fveq2d 5691 . . . . . . . . . . . 12 fldt t
285284fveq1d 5689 . . . . . . . . . . 11 fldt t
28682cnfldtopon 18770 . . . . . . . . . . . . . . 15 fld TopOn
287266adantr 452 . . . . . . . . . . . . . . 15
288 resttopon 17179 . . . . . . . . . . . . . . 15 fld TopOn fldt TopOn
289286, 287, 288sylancr 645 . . . . . . . . . . . . . 14 fldt TopOn
290 topontop 16946 . . . . . . . . . . . . . 14 fldt TopOn fldt
291289, 290syl 16 . . . . . . . . . . . . 13 fldt
292282, 291eqeltrrd 2479 . . . . . . . . . . . 12 t
293 iooretop 18753 . . . . . . . . . . . . . 14
294293a1i 11 . . . . . . . . . . . . 13
2954adantr 452 . . . . . . . . . . . . . 14
296 restopn2 17195 . . . . . . . . . . . . . 14 t
29786, 295, 296sylancr 645 . . . . . . . . . . . . 13 t
298294, 273, 297mpbir2and 889 . . . . . . . . . . . 12 t
299 isopn3i 17101 . . . . . . . . . . . 12 t t t
300292, 298, 299syl2anc 643 . . . . . . . . . . 11 t
301285, 300eqtrd 2436 . . . . . . . . . 10 fldt
30241, 301eleqtrrd 2481 . . . . . . . . 9 fldt
303 undif1 3663 . . . . . . . . . . 11
304 ssequn2 3480 . . . . . . . . . . . 12
30542, 304sylib 189 . . . . . . . . . . 11
306303, 305syl5eq 2448 . . . . . . . . . 10
307306fveq2d 5691 . . . . . . . . 9 fldt fldt
308302, 307eleqtrrd 2481 . . . . . . . 8 fldt
309263, 59, 268, 82, 269, 308limcres 19726 . . . . . . 7 lim lim
31080, 61sstri 3317 . . . . . . . . 9
311310a1i 11 . . . . . . . 8
312171, 61sstri 3317 . . . . . . . . 9
313312a1i 11 . . . . . . . 8
31459sselda 3308 . . . . . . . . . . 11
315314, 261syldan 457 . . . . . . . . . 10
316 eqid 2404 . . . . . . . . . 10
317315, 316fmptd 5852 . . . . . . . . 9
31854feq2d 5540 . . . . . . . . 9