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

environ

vocabularies HIDDEN, PARTFUN1, NUMBERS, REAL_1, SEQ_1, SUBSET_1, FCONT_1, ARYTM_3, RELAT_1, LIMFUNC3, SEQ_2, ORDINAL2, TARSKI, XBOOLE_0, FUNCT_2, FUNCT_1, LIMFUNC2, LIMFUNC1, RCOMP_1, CARD_1, XXREAL_1, ARYTM_1, FDIFF_1, VALUED_1, XXREAL_0, NAT_1, ASYMPT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, RELSET_1, PARTFUN1, RFUNCT_1, RCOMP_1, FCONT_1, FDIFF_1, LIMFUNC1, LIMFUNC2, LIMFUNC3, XXREAL_0;
definitions TARSKI;
theorems TARSKI, NAT_1, RFUNCT_1, RCOMP_1, FCONT_1, FDIFF_1, ROLLE, SEQ_2, SEQ_4, LIMFUNC2, LIMFUNC1, LIMFUNC3, ZFMISC_1, FUNCT_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, VALUED_1, XXREAL_1, XXREAL_2, FUNCT_2, VALUED_0, ORDINAL1, SEQ_1;
schemes FUNCT_2;
registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, RCOMP_1, VALUED_0, XXREAL_2, XBOOLE_0, SEQ_4, FUNCT_2, SEQ_1, SEQ_2;
constructors HIDDEN, PARTFUN1, FUNCOP_1, REAL_1, NAT_1, SEQ_2, SEQM_3, PROB_1, RCOMP_1, RFUNCT_1, RFUNCT_2, FCONT_1, LIMFUNC1, FDIFF_1, LIMFUNC2, LIMFUNC3, VALUED_1, XXREAL_2, RELSET_1, SEQ_4, COMSEQ_2, SEQ_1;
requirements HIDDEN, SUBSET, BOOLE, ARITHM, NUMERALS;
equalities PROB_1, LIMFUNC1;
expansions TARSKI;


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

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

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

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 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )
proof end;

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 & N c= dom g & f is_differentiable_on N & g is_differentiable_on N & N \ {x0} c= dom (f / g) & N c= dom ((f `| N) / (g `| N)) & f . x0 = 0 & g . x0 = 0 & (f `| N) / (g `| N) is_divergent_to+infty_in x0 ) holds
f / g is_divergent_to+infty_in x0
proof end;

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 & N c= dom g & f is_differentiable_on N & g is_differentiable_on N & N \ {x0} c= dom (f / g) & N c= dom ((f `| N) / (g `| N)) & f . x0 = 0 & g . x0 = 0 & (f `| N) / (g `| N) is_divergent_to-infty_in x0 ) holds
f / g is_divergent_to-infty_in x0
proof end;

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

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

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 & N c= dom g & f is_differentiable_on N & g is_differentiable_on N & N \ {x0} c= dom (f / g) & N c= dom ((f `| N) / (g `| N)) & f . x0 = 0 & g . x0 = 0 & (f `| N) / (g `| N) is_convergent_in x0 ) holds
( f / g is_convergent_in x0 & ex N being Neighbourhood of x0 st lim ((f / g),x0) = lim (((f `| N) / (g `| N)),x0) )
proof end;

:: 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 & N c= dom g & f is_differentiable_on N & g is_differentiable_on N & N \ {x0} c= dom (f / g) & N c= dom ((f `| N) / (g `| N)) & f . x0 = 0 & g . x0 = 0 & (f `| N) / (g `| N) is_continuous_in x0 ) holds
( f / g is_convergent_in x0 & lim ((f / g),x0) = (diff (f,x0)) / (diff (g,x0)) )
proof end;