Metamath Proof Explorer


Theorem lhop1

Description: L'Hôpital's Rule for limits from the right. If F and G are differentiable real functions on ( A , B ) , and F and G both approach 0 at A , and G ( x ) and G ' ( x ) are not zero on ( A , B ) , and the limit of F ' ( x ) / G ' ( x ) at A is C , then the limit F ( x ) / G ( x ) at A also exists and equals C . (Contributed by Mario Carneiro, 29-Dec-2016)

Ref Expression
Hypotheses lhop1.a φ A
lhop1.b φ B *
lhop1.l φ A < B
lhop1.f φ F : A B
lhop1.g φ G : A B
lhop1.if φ dom F = A B
lhop1.ig φ dom G = A B
lhop1.f0 φ 0 F lim A
lhop1.g0 φ 0 G lim A
lhop1.gn0 φ ¬ 0 ran G
lhop1.gd0 φ ¬ 0 ran G
lhop1.c φ C z A B F z G z lim A
Assertion lhop1 φ C z A B F z G z lim A

Proof

Step Hyp Ref Expression
1 lhop1.a φ A
2 lhop1.b φ B *
3 lhop1.l φ A < B
4 lhop1.f φ F : A B
5 lhop1.g φ G : A B
6 lhop1.if φ dom F = A B
7 lhop1.ig φ dom G = A B
8 lhop1.f0 φ 0 F lim A
9 lhop1.g0 φ 0 G lim A
10 lhop1.gn0 φ ¬ 0 ran G
11 lhop1.gd0 φ ¬ 0 ran G
12 lhop1.c φ C z A B F z G z lim A
13 simpr φ x + x +
14 13 rphalfcld φ x + x 2 +
15 breq2 e = x 2 z A B F z G z y C < e z A B F z G z y C < x 2
16 15 imbi2d e = x 2 y A y A < d z A B F z G z y C < e y A y A < d z A B F z G z y C < x 2
17 16 rexralbidv e = x 2 d + y A B y A y A < d z A B F z G z y C < e d + y A B y A y A < d z A B F z G z y C < x 2
18 17 rspcv x 2 + e + d + y A B y A y A < d z A B F z G z y C < e d + y A B y A y A < d z A B F z G z y C < x 2
19 14 18 syl φ x + e + d + y A B y A y A < d z A B F z G z y C < e d + y A B y A y A < d z A B F z G z y C < x 2
20 rabid v v A B | v A < d v A B v A < d
21 eliooord v A B A < v v < B
22 21 adantl φ x + d + v A B A < v v < B
23 22 simprd φ x + d + v A B v < B
24 23 biantrurd φ x + d + v A B v < d + A v < B v < d + A
25 ioossre A B
26 simpr φ x + d + v A B v A B
27 25 26 sselid φ x + d + v A B v
28 1 ad3antrrr φ x + d + v A B A
29 simpr φ x + d + d +
30 29 rpred φ x + d + d
31 30 adantr φ x + d + v A B d
32 27 28 31 ltsubaddd φ x + d + v A B v A < d v < d + A
33 27 rexrd φ x + d + v A B v *
34 2 ad3antrrr φ x + d + v A B B *
35 1 ad2antrr φ x + d + A
36 30 35 readdcld φ x + d + d + A
37 36 rexrd φ x + d + d + A *
38 37 adantr φ x + d + v A B d + A *
39 xrltmin v * B * d + A * v < if B d + A B d + A v < B v < d + A
40 33 34 38 39 syl3anc φ x + d + v A B v < if B d + A B d + A v < B v < d + A
41 24 32 40 3bitr4rd φ x + d + v A B v < if B d + A B d + A v A < d
42 28 rexrd φ x + d + v A B A *
43 34 38 ifcld φ x + d + v A B if B d + A B d + A *
44 22 simpld φ x + d + v A B A < v
45 elioo5 A * if B d + A B d + A * v * v A if B d + A B d + A A < v v < if B d + A B d + A
46 45 baibd A * if B d + A B d + A * v * A < v v A if B d + A B d + A v < if B d + A B d + A
47 42 43 33 44 46 syl31anc φ x + d + v A B v A if B d + A B d + A v < if B d + A B d + A
48 28 27 44 ltled φ x + d + v A B A v
49 28 27 48 abssubge0d φ x + d + v A B v A = v A
50 49 breq1d φ x + d + v A B v A < d v A < d
51 41 47 50 3bitr4d φ x + d + v A B v A if B d + A B d + A v A < d
52 51 rabbi2dva φ x + d + A B A if B d + A B d + A = v A B | v A < d
53 2 ad2antrr φ x + d + B *
54 xrmin1 B * d + A * if B d + A B d + A B
55 53 37 54 syl2anc φ x + d + if B d + A B d + A B
56 iooss2 B * if B d + A B d + A B A if B d + A B d + A A B
57 53 55 56 syl2anc φ x + d + A if B d + A B d + A A B
58 sseqin2 A if B d + A B d + A A B A B A if B d + A B d + A = A if B d + A B d + A
59 57 58 sylib φ x + d + A B A if B d + A B d + A = A if B d + A B d + A
60 52 59 eqtr3d φ x + d + v A B | v A < d = A if B d + A B d + A
61 60 eleq2d φ x + d + v v A B | v A < d v A if B d + A B d + A
62 20 61 bitr3id φ x + d + v A B v A < d v A if B d + A B d + A
63 lbioo ¬ A A B
64 eleq1 y = A y A B A A B
65 63 64 mtbiri y = A ¬ y A B
66 65 necon2ai y A B y A
67 66 biantrurd y A B y A < d y A y A < d
68 67 bicomd y A B y A y A < d y A < d
69 fveq2 z = y F z = F y
70 fveq2 z = y G z = G y
71 69 70 oveq12d z = y F z G z = F y G y
72 eqid z A B F z G z = z A B F z G z
73 ovex F z G z V
74 71 72 73 fvmpt3i y A B z A B F z G z y = F y G y
75 74 fvoveq1d y A B z A B F z G z y C = F y G y C
76 75 breq1d y A B z A B F z G z y C < x 2 F y G y C < x 2
77 68 76 imbi12d y A B y A y A < d z A B F z G z y C < x 2 y A < d F y G y C < x 2
78 77 ralbiia y A B y A y A < d z A B F z G z y C < x 2 y A B y A < d F y G y C < x 2
79 fvoveq1 v = y v A = y A
80 79 breq1d v = y v A < d y A < d
81 80 ralrab y v A B | v A < d F y G y C < x 2 y A B y A < d F y G y C < x 2
82 78 81 bitr4i y A B y A y A < d z A B F z G z y C < x 2 y v A B | v A < d F y G y C < x 2
83 60 adantrr φ x + d + v A if B d + A B d + A v A B | v A < d = A if B d + A B d + A
84 83 raleqdv φ x + d + v A if B d + A B d + A y v A B | v A < d F y G y C < x 2 y A if B d + A B d + A F y G y C < x 2
85 1 ad2antrr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 A
86 2 ad2antrr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 B *
87 3 ad2antrr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 A < B
88 4 ad2antrr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 F : A B
89 5 ad2antrr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 G : A B
90 6 ad2antrr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 dom F = A B
91 7 ad2antrr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 dom G = A B
92 8 ad2antrr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 0 F lim A
93 9 ad2antrr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 0 G lim A
94 10 ad2antrr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 ¬ 0 ran G
95 11 ad2antrr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 ¬ 0 ran G
96 12 ad2antrr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 C z A B F z G z lim A
97 14 adantr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 x 2 +
98 85 rexrd φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 A *
99 simprll φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 d +
100 99 rpred φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 d
101 100 85 readdcld φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 d + A
102 iocssre A * d + A A d + A
103 98 101 102 syl2anc φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 A d + A
104 86 adantr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 B d + A B *
105 100 adantr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 ¬ B d + A d
106 85 adantr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 ¬ B d + A A
107 105 106 readdcld φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 ¬ B d + A d + A
108 107 rexrd φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 ¬ B d + A d + A *
109 104 108 ifclda φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 if B d + A B d + A *
110 85 99 ltaddrp2d φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 A < d + A
111 101 rexrd φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 d + A *
112 xrltmin A * B * d + A * A < if B d + A B d + A A < B A < d + A
113 98 86 111 112 syl3anc φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 A < if B d + A B d + A A < B A < d + A
114 87 110 113 mpbir2and φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 A < if B d + A B d + A
115 xrmin2 B * d + A * if B d + A B d + A d + A
116 86 111 115 syl2anc φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 if B d + A B d + A d + A
117 elioc1 A * d + A * if B d + A B d + A A d + A if B d + A B d + A * A < if B d + A B d + A if B d + A B d + A d + A
118 98 111 117 syl2anc φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 if B d + A B d + A A d + A if B d + A B d + A * A < if B d + A B d + A if B d + A B d + A d + A
119 109 114 116 118 mpbir3and φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 if B d + A B d + A A d + A
120 103 119 sseldd φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 if B d + A B d + A
121 86 111 54 syl2anc φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 if B d + A B d + A B
122 simprlr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 v A if B d + A B d + A
123 simprr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 y A if B d + A B d + A F y G y C < x 2
124 eqid A + r 2 = A + r 2
125 85 86 87 88 89 90 91 92 93 94 95 96 97 120 121 122 123 124 lhop1lem φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 F v G v C < 2 x 2
126 13 rpcnd φ x + x
127 2cnd φ x + 2
128 2ne0 2 0
129 128 a1i φ x + 2 0
130 126 127 129 divcan2d φ x + 2 x 2 = x
131 130 adantr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 2 x 2 = x
132 125 131 breqtrd φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 F v G v C < x
133 132 expr φ x + d + v A if B d + A B d + A y A if B d + A B d + A F y G y C < x 2 F v G v C < x
134 84 133 sylbid φ x + d + v A if B d + A B d + A y v A B | v A < d F y G y C < x 2 F v G v C < x
135 82 134 syl5bi φ x + d + v A if B d + A B d + A y A B y A y A < d z A B F z G z y C < x 2 F v G v C < x
136 135 expr φ x + d + v A if B d + A B d + A y A B y A y A < d z A B F z G z y C < x 2 F v G v C < x
137 62 136 sylbid φ x + d + v A B v A < d y A B y A y A < d z A B F z G z y C < x 2 F v G v C < x
138 137 expdimp φ x + d + v A B v A < d y A B y A y A < d z A B F z G z y C < x 2 F v G v C < x
139 fveq2 z = v F z = F v
140 fveq2 z = v G z = G v
141 139 140 oveq12d z = v F z G z = F v G v
142 eqid z A B F z G z = z A B F z G z
143 ovex F z G z V
144 141 142 143 fvmpt3i v A B z A B F z G z v = F v G v
145 144 fvoveq1d v A B z A B F z G z v C = F v G v C
146 145 breq1d v A B z A B F z G z v C < x F v G v C < x
147 146 imbi2d v A B y A B y A y A < d z A B F z G z y C < x 2 z A B F z G z v C < x y A B y A y A < d z A B F z G z y C < x 2 F v G v C < x
148 147 adantl φ x + d + v A B y A B y A y A < d z A B F z G z y C < x 2 z A B F z G z v C < x y A B y A y A < d z A B F z G z y C < x 2 F v G v C < x
149 138 148 sylibrd φ x + d + v A B v A < d y A B y A y A < d z A B F z G z y C < x 2 z A B F z G z v C < x
150 149 adantld φ x + d + v A B v A v A < d y A B y A y A < d z A B F z G z y C < x 2 z A B F z G z v C < x
151 150 com23 φ x + d + v A B y A B y A y A < d z A B F z G z y C < x 2 v A v A < d z A B F z G z v C < x
152 151 ralrimdva φ x + d + y A B y A y A < d z A B F z G z y C < x 2 v A B v A v A < d z A B F z G z v C < x
153 152 reximdva φ x + d + y A B y A y A < d z A B F z G z y C < x 2 d + v A B v A v A < d z A B F z G z v C < x
154 19 153 syld φ x + e + d + y A B y A y A < d z A B F z G z y C < e d + v A B v A v A < d z A B F z G z v C < x
155 154 ralrimdva φ e + d + y A B y A y A < d z A B F z G z y C < e x + d + v A B v A v A < d z A B F z G z v C < x
156 155 anim2d φ C e + d + y A B y A y A < d z A B F z G z y C < e C x + d + v A B v A v A < d z A B F z G z v C < x
157 dvf F : dom F
158 6 feq2d φ F : dom F F : A B
159 157 158 mpbii φ F : A B
160 159 ffvelrnda φ z A B F z
161 dvf G : dom G
162 7 feq2d φ G : dom G G : A B
163 161 162 mpbii φ G : A B
164 163 ffvelrnda φ z A B G z
165 11 adantr φ z A B ¬ 0 ran G
166 163 ffnd φ G Fn A B
167 fnfvelrn G Fn A B z A B G z ran G
168 166 167 sylan φ z A B G z ran G
169 eleq1 G z = 0 G z ran G 0 ran G
170 168 169 syl5ibcom φ z A B G z = 0 0 ran G
171 170 necon3bd φ z A B ¬ 0 ran G G z 0
172 165 171 mpd φ z A B G z 0
173 160 164 172 divcld φ z A B F z G z
174 173 fmpttd φ z A B F z G z : A B
175 ax-resscn
176 25 175 sstri A B
177 176 a1i φ A B
178 1 recnd φ A
179 174 177 178 ellimc3 φ C z A B F z G z lim A C e + d + y A B y A y A < d z A B F z G z y C < e
180 4 ffvelrnda φ z A B F z
181 180 recnd φ z A B F z
182 5 ffvelrnda φ z A B G z
183 182 recnd φ z A B G z
184 10 adantr φ z A B ¬ 0 ran G
185 5 ffnd φ G Fn A B
186 fnfvelrn G Fn A B z A B G z ran G
187 185 186 sylan φ z A B G z ran G
188 eleq1 G z = 0 G z ran G 0 ran G
189 187 188 syl5ibcom φ z A B G z = 0 0 ran G
190 189 necon3bd φ z A B ¬ 0 ran G G z 0
191 184 190 mpd φ z A B G z 0
192 181 183 191 divcld φ z A B F z G z
193 192 fmpttd φ z A B F z G z : A B
194 193 177 178 ellimc3 φ C z A B F z G z lim A C x + d + v A B v A v A < d z A B F z G z v C < x
195 156 179 194 3imtr4d φ C z A B F z G z lim A C z A B F z G z lim A
196 12 195 mpd φ C z A B F z G z lim A