:: The de l'Hospital Theorem
:: by Ma{\l}gorzata Korolkiewicz
::
:: Received February 20, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

theorem :: L_HOSPIT:1
for f being PartFunc of REAL,REAL
for x0 being Real st f is_continuous_in x0 &amp; ( for r1, r2 being Real st r1 < x0 &amp; x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 &amp; g1 < x0 &amp; g1 in dom f &amp; g2 < r2 &amp; x0 < g2 &amp; g2 in dom f ) ) holds
f is_convergent_in x0
proofend;

theorem Th2: :: L_HOSPIT:2
for f being PartFunc of REAL,REAL
for x0, t being Real holds
( f is_right_convergent_in x0 &amp; lim_right (f,x0) = t iff ( ( for r being Real st x0 < r holds
ex t being Real st
( t < r &amp; x0 < t &amp; t in dom f ) ) &amp; ( for a being Real_Sequence st a is convergent &amp; lim a = x0 &amp; rng a c= (dom f) /\ (right_open_halfline x0) holds
( f /* a is convergent &amp; lim (f /* a) = t ) ) ) )
proofend;

theorem Th3: :: L_HOSPIT:3
for f being PartFunc of REAL,REAL
for x0, t being Real holds
( f is_left_convergent_in x0 &amp; lim_left (f,x0) = t iff ( ( for r being Real st r < x0 holds
ex t being Real st
( r < t &amp; t < x0 &amp; t in dom f ) ) &amp; ( for a being Real_Sequence st a is convergent &amp; lim a = x0 &amp; rng a c= (dom f) /\ (left_open_halfline x0) holds
( f /* a is convergent &amp; lim (f /* a) = t ) ) ) )
proofend;

theorem Th4: :: L_HOSPIT:4
for f being PartFunc of REAL,REAL
for x0 being Real st ex N being Neighbourhood of x0 st N \ {x0} c= dom f holds
for r1, r2 being Real st r1 < x0 &amp; x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 &amp; g1 < x0 &amp; g1 in dom f &amp; g2 < r2 &amp; x0 < g2 &amp; g2 in dom f )
proofend;

theorem :: L_HOSPIT:5
for f, g being PartFunc of REAL,REAL
for x0 being Real st ex N being Neighbourhood of x0 st
( N c= dom f &amp; N c= dom g &amp; f is_differentiable_on N &amp; g is_differentiable_on N &amp; N \ {x0} c= dom (f / g) &amp; N c= dom ((f `| N) / (g `| N)) &amp; f . x0 = 0 &amp; g . x0 = 0 &amp; (f `| N) / (g `| N) is_divergent_to+infty_in x0 ) holds
f / g is_divergent_to+infty_in x0
proofend;

theorem :: L_HOSPIT:6
for f, g being PartFunc of REAL,REAL
for x0 being Real st ex N being Neighbourhood of x0 st
( N c= dom f &amp; N c= dom g &amp; f is_differentiable_on N &amp; g is_differentiable_on N &amp; N \ {x0} c= dom (f / g) &amp; N c= dom ((f `| N) / (g `| N)) &amp; f . x0 = 0 &amp; g . x0 = 0 &amp; (f `| N) / (g `| N) is_divergent_to-infty_in x0 ) holds
f / g is_divergent_to-infty_in x0
proofend;

theorem :: L_HOSPIT:7
for f, g being PartFunc of REAL,REAL
for x0 being Real st x0 in (dom f) /\ (dom g) &amp; ex r being Real st
( r > 0 &amp; [.x0,(x0 + r).] c= dom f &amp; [.x0,(x0 + r).] c= dom g &amp; f is_differentiable_on ].x0,(x0 + r).[ &amp; g is_differentiable_on ].x0,(x0 + r).[ &amp; ].x0,(x0 + r).[ c= dom (f / g) &amp; [.x0,(x0 + r).] c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) &amp; f . x0 = 0 &amp; g . x0 = 0 &amp; f is_continuous_in x0 &amp; g is_continuous_in x0 &amp; (f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[) is_right_convergent_in x0 ) holds
( f / g is_right_convergent_in x0 &amp; ex r being Real st
( r > 0 &amp; lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) )
proofend;

theorem :: L_HOSPIT:8
for f, g being PartFunc of REAL,REAL
for x0 being Real st x0 in (dom f) /\ (dom g) &amp; ex r being Real st
( r > 0 &amp; [.(x0 - r),x0.] c= dom f &amp; [.(x0 - r),x0.] c= dom g &amp; f is_differentiable_on ].(x0 - r),x0.[ &amp; g is_differentiable_on ].(x0 - r),x0.[ &amp; ].(x0 - r),x0.[ c= dom (f / g) &amp; [.(x0 - r),x0.] c= dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) &amp; f . x0 = 0 &amp; g . x0 = 0 &amp; f is_continuous_in x0 &amp; g is_continuous_in x0 &amp; (f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[) is_left_convergent_in x0 ) holds
( f / g is_left_convergent_in x0 &amp; ex r being Real st
( r > 0 &amp; lim_left ((f / g),x0) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) ) )
proofend;

theorem :: L_HOSPIT:9
for f, g being PartFunc of REAL,REAL
for x0 being Real st ex N being Neighbourhood of x0 st
( N c= dom f &amp; N c= dom g &amp; f is_differentiable_on N &amp; g is_differentiable_on N &amp; N \ {x0} c= dom (f / g) &amp; N c= dom ((f `| N) / (g `| N)) &amp; f . x0 = 0 &amp; g . x0 = 0 &amp; (f `| N) / (g `| N) is_convergent_in x0 ) holds
( f / g is_convergent_in x0 &amp; ex N being Neighbourhood of x0 st lim ((f / g),x0) = lim (((f `| N) / (g `| N)),x0) )
proofend;

:: [WP: ] l'Hospital_Theorem
theorem :: L_HOSPIT:10
for f, g being PartFunc of REAL,REAL
for x0 being Real st ex N being Neighbourhood of x0 st
( N c= dom f &amp; N c= dom g &amp; f is_differentiable_on N &amp; g is_differentiable_on N &amp; N \ {x0} c= dom (f / g) &amp; N c= dom ((f `| N) / (g `| N)) &amp; f . x0 = 0 &amp; g . x0 = 0 &amp; (f `| N) / (g `| N) is_continuous_in x0 ) holds
( f / g is_convergent_in x0 &amp; lim ((f / g),x0) = (diff (f,x0)) / (diff (g,x0)) )
proofend;