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

Theorem lhop 23047
 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 . This is Metamath 100 proof #64. (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 2471 . . . . 5
21rexmet 21887 . . . 4
32a1i 11 . . 3
4 lhop.i . . 3
5 lhop.b . . 3
6 eqid 2471 . . . . 5
71, 6tgioo 21892 . . . 4
87mopni2 21586 . . 3
93, 4, 5, 8syl3anc 1292 . 2
10 elssuni 4219 . . . . . . . . 9
11 uniretop 21861 . . . . . . . . 9
1210, 11syl6sseqr 3465 . . . . . . . 8
134, 12syl 17 . . . . . . 7
1413, 5sseldd 3419 . . . . . 6
15 rpre 11331 . . . . . 6
161bl2ioo 21888 . . . . . 6
1714, 15, 16syl2an 485 . . . . 5
1817sseq1d 3445 . . . 4
1914adantr 472 . . . . . . . . . . 11
20 simprl 772 . . . . . . . . . . . 12
2120rpred 11364 . . . . . . . . . . 11
2219, 21resubcld 10068 . . . . . . . . . 10
2322rexrd 9708 . . . . . . . . 9
2419, 20ltsubrpd 11393 . . . . . . . . 9
25 lhop.f . . . . . . . . . . 11
2625adantr 472 . . . . . . . . . 10
27 ssun1 3588 . . . . . . . . . . . 12
28 unass 3582 . . . . . . . . . . . . . . 15
29 uncom 3569 . . . . . . . . . . . . . . . 16
3029uneq1i 3575 . . . . . . . . . . . . . . 15
3128, 30eqtr3i 2495 . . . . . . . . . . . . . 14
3219rexrd 9708 . . . . . . . . . . . . . . 15
3319, 21readdcld 9688 . . . . . . . . . . . . . . . 16
3433rexrd 9708 . . . . . . . . . . . . . . 15
3519, 20ltaddrpd 11394 . . . . . . . . . . . . . . 15
36 ioojoin 11789 . . . . . . . . . . . . . . 15
3723, 32, 34, 24, 35, 36syl32anc 1300 . . . . . . . . . . . . . 14
3831, 37syl5eq 2517 . . . . . . . . . . . . 13
39 elioo2 11702 . . . . . . . . . . . . . . . . 17
4023, 34, 39syl2anc 673 . . . . . . . . . . . . . . . 16
4119, 24, 35, 40mpbir3and 1213 . . . . . . . . . . . . . . 15
4241snssd 4108 . . . . . . . . . . . . . 14
43 incom 3616 . . . . . . . . . . . . . . 15
44 ubioo 11693 . . . . . . . . . . . . . . . . . 18
45 lbioo 11692 . . . . . . . . . . . . . . . . . 18
4644, 45pm3.2ni 872 . . . . . . . . . . . . . . . . 17
47 elun 3565 . . . . . . . . . . . . . . . . 17
4846, 47mtbir 306 . . . . . . . . . . . . . . . 16
49 disjsn 4023 . . . . . . . . . . . . . . . 16
5048, 49mpbir 214 . . . . . . . . . . . . . . 15
5143, 50eqtri 2493 . . . . . . . . . . . . . 14
52 uneqdifeq 3847 . . . . . . . . . . . . . 14
5342, 51, 52sylancl 675 . . . . . . . . . . . . 13
5438, 53mpbid 215 . . . . . . . . . . . 12
5527, 54syl5sseqr 3467 . . . . . . . . . . 11
56 ssdif 3557 . . . . . . . . . . . . . 14
5756ad2antll 743 . . . . . . . . . . . . 13
58 lhop.d . . . . . . . . . . . . 13
5957, 58syl6sseqr 3465 . . . . . . . . . . . 12
60 lhop.if . . . . . . . . . . . . . 14
61 ax-resscn 9614 . . . . . . . . . . . . . . . 16
6261a1i 11 . . . . . . . . . . . . . . 15
63 fss 5749 . . . . . . . . . . . . . . . 16
6425, 61, 63sylancl 675 . . . . . . . . . . . . . . 15
65 lhop.a . . . . . . . . . . . . . . 15
6662, 64, 65dvbss 22935 . . . . . . . . . . . . . 14
6760, 66sstrd 3428 . . . . . . . . . . . . 13
6867adantr 472 . . . . . . . . . . . 12
6959, 68sstrd 3428 . . . . . . . . . . 11
7055, 69sstrd 3428 . . . . . . . . . 10
7126, 70fssresd 5762 . . . . . . . . 9
72 lhop.g . . . . . . . . . . 11
7372adantr 472 . . . . . . . . . 10
7473, 70fssresd 5762 . . . . . . . . 9
7561a1i 11 . . . . . . . . . . . . 13
7664adantr 472 . . . . . . . . . . . . 13
7765adantr 472 . . . . . . . . . . . . 13
78 ioossre 11721 . . . . . . . . . . . . . 14
7978a1i 11 . . . . . . . . . . . . 13
80 eqid 2471 . . . . . . . . . . . . . 14 fld fld
8180tgioo2 21899 . . . . . . . . . . . . . 14 fldt
8280, 81dvres 22945 . . . . . . . . . . . . 13
8375, 76, 77, 79, 82syl22anc 1293 . . . . . . . . . . . 12
84 retop 21860 . . . . . . . . . . . . . 14
85 iooretop 21864 . . . . . . . . . . . . . 14
86 isopn3i 20175 . . . . . . . . . . . . . 14
8784, 85, 86mp2an 686 . . . . . . . . . . . . 13
8887reseq2i 5108 . . . . . . . . . . . 12
8983, 88syl6eq 2521 . . . . . . . . . . 11
9089dmeqd 5042 . . . . . . . . . 10
9155, 59sstrd 3428 . . . . . . . . . . . 12
9260adantr 472 . . . . . . . . . . . 12
9391, 92sstrd 3428 . . . . . . . . . . 11
94 ssdmres 5132 . . . . . . . . . . 11
9593, 94sylib 201 . . . . . . . . . 10
9690, 95eqtrd 2505 . . . . . . . . 9
97 fss 5749 . . . . . . . . . . . . . . 15
9872, 61, 97sylancl 675 . . . . . . . . . . . . . 14
9998adantr 472 . . . . . . . . . . . . 13
10080, 81dvres 22945 . . . . . . . . . . . . 13
10175, 99, 77, 79, 100syl22anc 1293 . . . . . . . . . . . 12
10287reseq2i 5108 . . . . . . . . . . . 12
103101, 102syl6eq 2521 . . . . . . . . . . 11
104103dmeqd 5042 . . . . . . . . . 10
105 lhop.ig . . . . . . . . . . . . 13
106105adantr 472 . . . . . . . . . . . 12
10791, 106sstrd 3428 . . . . . . . . . . 11
108 ssdmres 5132 . . . . . . . . . . 11
109107, 108sylib 201 . . . . . . . . . 10
110104, 109eqtrd 2505 . . . . . . . . 9
111 limcresi 22919 . . . . . . . . . 10 lim lim
112 lhop.f0 . . . . . . . . . . 11 lim
113112adantr 472 . . . . . . . . . 10 lim
114111, 113sseldi 3416 . . . . . . . . 9 lim
115 limcresi 22919 . . . . . . . . . 10 lim lim
116 lhop.g0 . . . . . . . . . . 11 lim
117116adantr 472 . . . . . . . . . 10 lim
118115, 117sseldi 3416 . . . . . . . . 9 lim
119 df-ima 4852 . . . . . . . . . . 11
120 imass2 5210 . . . . . . . . . . . 12
12191, 120syl 17 . . . . . . . . . . 11
122119, 121syl5eqssr 3463 . . . . . . . . . 10
123 lhop.gn0 . . . . . . . . . . 11
124123adantr 472 . . . . . . . . . 10
125122, 124ssneldd 3421 . . . . . . . . 9
126103rneqd 5068 . . . . . . . . . . . 12
127 df-ima 4852 . . . . . . . . . . . 12
128126, 127syl6eqr 2523 . . . . . . . . . . 11
129 imass2 5210 . . . . . . . . . . . 12
13091, 129syl 17 . . . . . . . . . . 11
131128, 130eqsstrd 3452 . . . . . . . . . 10
132 lhop.gd0 . . . . . . . . . . 11
133132adantr 472 . . . . . . . . . 10
134131, 133ssneldd 3421 . . . . . . . . 9
135 limcresi 22919 . . . . . . . . . . 11 lim lim
13691resmptd 5162 . . . . . . . . . . . . 13
13789fveq1d 5881 . . . . . . . . . . . . . . . 16
138 fvres 5893 . . . . . . . . . . . . . . . 16
139137, 138sylan9eq 2525 . . . . . . . . . . . . . . 15
140103fveq1d 5881 . . . . . . . . . . . . . . . 16
141 fvres 5893 . . . . . . . . . . . . . . . 16
142140, 141sylan9eq 2525 . . . . . . . . . . . . . . 15
143139, 142oveq12d 6326 . . . . . . . . . . . . . 14
144143mpteq2dva 4482 . . . . . . . . . . . . 13
145136, 144eqtr4d 2508 . . . . . . . . . . . 12
146145oveq1d 6323 . . . . . . . . . . 11 lim lim
147135, 146syl5sseq 3466 . . . . . . . . . 10 lim lim
148 lhop.c . . . . . . . . . . 11 lim
149148adantr 472 . . . . . . . . . 10 lim
150147, 149sseldd 3419 . . . . . . . . 9 lim
15123, 19, 24, 71, 74, 96, 110, 114, 118, 125, 134, 150lhop2 23046 . . . . . . . 8 lim
15255resmptd 5162 . . . . . . . . . 10
153 fvres 5893 . . . . . . . . . . . 12
154 fvres 5893 . . . . . . . . . . . 12
155153, 154oveq12d 6326 . . . . . . . . . . 11
156155mpteq2ia 4478 . . . . . . . . . 10
157152, 156syl6eqr 2523 . . . . . . . . 9
158157oveq1d 6323 . . . . . . . 8 lim lim
159151, 158eleqtrrd 2552 . . . . . . 7 lim
160 ssun2 3589 . . . . . . . . . . . 12
161160, 54syl5sseqr 3467 . . . . . . . . . . 11
162161, 69sstrd 3428 . . . . . . . . . 10
16326, 162fssresd 5762 . . . . . . . . 9
16473, 162fssresd 5762 . . . . . . . . 9
165 ioossre 11721 . . . . . . . . . . . . . 14
166165a1i 11 . . . . . . . . . . . . 13
16780, 81dvres 22945 . . . . . . . . . . . . 13
16875, 76, 77, 166, 167syl22anc 1293 . . . . . . . . . . . 12
169 iooretop 21864 . . . . . . . . . . . . . 14
170 isopn3i 20175 . . . . . . . . . . . . . 14
17184, 169, 170mp2an 686 . . . . . . . . . . . . 13
172171reseq2i 5108 . . . . . . . . . . . 12
173168, 172syl6eq 2521 . . . . . . . . . . 11
174173dmeqd 5042 . . . . . . . . . 10
175161, 59sstrd 3428 . . . . . . . . . . . 12
176175, 92sstrd 3428 . . . . . . . . . . 11
177 ssdmres 5132 . . . . . . . . . . 11
178176, 177sylib 201 . . . . . . . . . 10
179174, 178eqtrd 2505 . . . . . . . . 9
18080, 81dvres 22945 . . . . . . . . . . . . 13
18175, 99, 77, 166, 180syl22anc 1293 . . . . . . . . . . . 12
182171reseq2i 5108 . . . . . . . . . . . 12
183181, 182syl6eq 2521 . . . . . . . . . . 11
184183dmeqd 5042 . . . . . . . . . 10
185175, 106sstrd 3428 . . . . . . . . . . 11
186 ssdmres 5132 . . . . . . . . . . 11
187185, 186sylib 201 . . . . . . . . . 10
188184, 187eqtrd 2505 . . . . . . . . 9
189 limcresi 22919 . . . . . . . . . 10 lim lim
190189, 113sseldi 3416 . . . . . . . . 9 lim
191 limcresi 22919 . . . . . . . . . 10 lim lim
192191, 117sseldi 3416 . . . . . . . . 9 lim
193 df-ima 4852 . . . . . . . . . . 11
194 imass2 5210 . . . . . . . . . . . 12
195175, 194syl 17 . . . . . . . . . . 11
196193, 195syl5eqssr 3463 . . . . . . . . . 10
197196, 124ssneldd 3421 . . . . . . . . 9
198183rneqd 5068 . . . . . . . . . . . 12
199 df-ima 4852 . . . . . . . . . . . 12
200198, 199syl6eqr 2523 . . . . . . . . . . 11
201 imass2 5210 . . . . . . . . . . . 12
202175, 201syl 17 . . . . . . . . . . 11
203200, 202eqsstrd 3452 . . . . . . . . . 10
204203, 133ssneldd 3421 . . . . . . . . 9
205 limcresi 22919 . . . . . . . . . . 11 lim lim
206175resmptd 5162 . . . . . . . . . . . . 13
207173fveq1d 5881 . . . . . . . . . . . . . . . 16
208 fvres 5893 . . . . . . . . . . . . . . . 16
209207, 208sylan9eq 2525 . . . . . . . . . . . . . . 15
210183fveq1d 5881 . . . . . . . . . . . . . . . 16
211 fvres 5893 . . . . . . . . . . . . . . . 16
212210, 211sylan9eq 2525 . . . . . . . . . . . . . . 15
213209, 212oveq12d 6326 . . . . . . . . . . . . . 14
214213mpteq2dva 4482 . . . . . . . . . . . . 13
215206, 214eqtr4d 2508 . . . . . . . . . . . 12
216215oveq1d 6323 . . . . . . . . . . 11 lim lim
217205, 216syl5sseq 3466 . . . . . . . . . 10 lim lim
218217, 149sseldd 3419 . . . . . . . . 9 lim
21919, 34, 35, 163, 164, 179, 188, 190, 192, 197, 204, 218lhop1 23045 . . . . . . . 8 lim
220161resmptd 5162 . . . . . . . . . 10
221 fvres 5893 . . . . . . . . . . . 12
222 fvres 5893 . . . . . . . . . . . 12
223221, 222oveq12d 6326 . . . . . . . . . . 11
224223mpteq2ia 4478 . . . . . . . . . 10
225220, 224syl6eqr 2523 . . . . . . . . 9
226225oveq1d 6323 . . . . . . . 8 lim lim
227219, 226eleqtrrd 2552 . . . . . . 7 lim
228159, 227elind 3609 . . . . . 6 lim lim
22959resmptd 5162 . . . . . . . 8
230229oveq1d 6323 . . . . . . 7 lim lim
23167sselda 3418 . . . . . . . . . . . . 13
23225ffvelrnda 6037 . . . . . . . . . . . . 13
233231, 232syldan 478 . . . . . . . . . . . 12
234233recnd 9687 . . . . . . . . . . 11
23572ffvelrnda 6037 . . . . . . . . . . . . 13
236231, 235syldan 478 . . . . . . . . . . . 12
237236recnd 9687 . . . . . . . . . . 11
238123adantr 472 . . . . . . . . . . . 12
239 ffn 5739 . . . . . . . . . . . . . . . . 17
24072, 239syl 17 . . . . . . . . . . . . . . . 16
241240adantr 472 . . . . . . . . . . . . . . 15
24267adantr 472 . . . . . . . . . . . . . . 15
243 simpr 468 . . . . . . . . . . . . . . 15
244 fnfvima 6161 . . . . . . . . . . . . . . 15
245241, 242, 243, 244syl3anc 1292 . . . . . . . . . . . . . 14
246 eleq1 2537 . . . . . . . . . . . . . 14
247245, 246syl5ibcom 228 . . . . . . . . . . . . 13
248247necon3bd 2657 . . . . . . . . . . . 12
249238, 248mpd 15 . . . . . . . . . . 11
250234, 237, 249divcld 10405 . . . . . . . . . 10
251250adantlr 729 . . . . . . . . 9
252 eqid 2471 . . . . . . . . 9
253251, 252fmptd 6061 . . . . . . . 8
254 difss 3549 . . . . . . . . . . 11
25558, 254eqsstri 3448 . . . . . . . . . 10
25613, 61syl6ss 3430 . . . . . . . . . 10
257255, 256syl5ss 3429 . . . . . . . . 9
258257adantr 472 . . . . . . . 8
259 eqid 2471 . . . . . . . 8 fldt fldt
26058uneq1i 3575 . . . . . . . . . . . . . . . . 17
261 undif1 3833 . . . . . . . . . . . . . . . . 17
262260, 261eqtri 2493 . . . . . . . . . . . . . . . 16
263 simprr 774 . . . . . . . . . . . . . . . . . 18
26442, 263sstrd 3428 . . . . . . . . . . . . . . . . 17
265 ssequn2 3598 . . . . . . . . . . . . . . . . 17
266264, 265sylib 201 . . . . . . . . . . . . . . . 16
267262, 266syl5eq 2517 . . . . . . . . . . . . . . 15
268267oveq2d 6324 . . . . . . . . . . . . . 14 fldt fldt
26913adantr 472 . . . . . . . . . . . . . . 15
270 eqid 2471 . . . . . . . . . . . . . . . 16
27180, 270rerest 21900 . . . . . . . . . . . . . . 15 fldt t
272269, 271syl 17 . . . . . . . . . . . . . 14 fldt t
273268, 272eqtrd 2505 . . . . . . . . . . . . 13 fldt t
274273fveq2d 5883 . . . . . . . . . . . 12 fldt t
275274fveq1d 5881 . . . . . . . . . . 11 fldt t
27680cnfldtopon 21881 . . . . . . . . . . . . . . 15 fld TopOn
277256adantr 472 . . . . . . . . . . . . . . 15
278 resttopon 20254 . . . . . . . . . . . . . . 15 fld TopOn fldt TopOn
279276, 277, 278sylancr 676 . . . . . . . . . . . . . 14 fldt TopOn
280 topontop 20018 . . . . . . . . . . . . . 14 fldt TopOn fldt
281279, 280syl 17 . . . . . . . . . . . . 13 fldt
282272, 281eqeltrrd 2550 . . . . . . . . . . . 12 t
283 iooretop 21864 . . . . . . . . . . . . . 14
284283a1i 11 . . . . . . . . . . . . 13
2854adantr 472 . . . . . . . . . . . . . 14
286 restopn2 20270 . . . . . . . . . . . . . 14 t
28784, 285, 286sylancr 676 . . . . . . . . . . . . 13 t
288284, 263, 287mpbir2and 936 . . . . . . . . . . . 12 t
289 isopn3i 20175 . . . . . . . . . . . 12 t t t
290282, 288, 289syl2anc 673 . . . . . . . . . . 11 t
291275, 290eqtrd 2505 . . . . . . . . . 10 fldt
29241, 291eleqtrrd 2552 . . . . . . . . 9 fldt
293 undif1 3833 . . . . . . . . . . 11
294 ssequn2 3598 . . . . . . . . . . . 12
29542, 294sylib 201 . . . . . . . . . . 11
296293, 295syl5eq 2517 . . . . . . . . . 10
297296fveq2d 5883 . . . . . . . . 9 fldt fldt
298292, 297eleqtrrd 2552 . . . . . . . 8 fldt
299253, 59, 258, 80, 259, 298limcres 22920 . . . . . . 7 lim lim
30078, 61sstri 3427 . . . . . . . . 9
301300a1i 11 . . . . . . . 8
302165, 61sstri 3427 . . . . . . . . 9
303302a1i 11 . . . . . . . 8
30459sselda 3418 . . . . . . . . . . 11
305304, 251syldan 478 . . . . . . . . . 10
306 eqid 2471 . . . . . . . . . 10
307305, 306fmptd 6061 . . . . . . . . 9
30854feq2d 5725 . . . . . . . . 9
309307, 308mpbid 215 . . . . . . . 8
310301, 303, 309limcun 22929 . . . . . . 7 lim lim lim
311230, 299, 3103eqtr3rd 2514 . . . . . 6 lim lim lim
312228, 311eleqtrd 2551 . . . . 5 lim
313312expr 626 . . . 4 lim
31418, 313sylbid 223 . . 3 lim
315314rexlimdva 2871 . 2 lim
3169, 315mpd 15 1 lim
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wo 375   wa 376   w3a 1007   wceq 1452   wcel 1904   wne 2641  wrex 2757   cdif 3387   cun 3388   cin 3389   wss 3390  c0 3722  csn 3959  cuni 4190   class class class wbr 4395   cmpt 4454   cxp 4837   cdm 4839   crn 4840   cres 4841  cima 4842   ccom 4843   wfn 5584  wf 5585  cfv 5589  (class class class)co 6308  cc 9555  cr 9556  cc0 9557   caddc 9560  cxr