The abstract of the Mizar article:

The de l'Hospital Theorem

by

Malgorzata Korolkiewicz

Received February 20, 1992

MML identifier: L_HOSPIT

[ Mizar article, MML identifier index ]

environ

 vocabulary PARTFUN1, SEQ_1, FCONT_1, RELAT_1, LIMFUNC3, SEQ_2, ORDINAL2,
      BOOLE, FUNCT_1, LIMFUNC2, LIMFUNC1, RCOMP_1, ARYTM_1, FDIFF_1, ARYTM_3,
      SEQM_3, ARYTM;
 notation TARSKI, XBOOLE_0, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1,
      NAT_1, SEQ_1, SEQ_2, SEQM_3, RELSET_1, PARTFUN1, RFUNCT_1, RCOMP_1,
      RFUNCT_2, FCONT_1, FDIFF_1, LIMFUNC1, LIMFUNC2, LIMFUNC3;
 constructors REAL_1, NAT_1, SEQ_2, SEQM_3, PROB_1, RFUNCT_1, RCOMP_1,
      RFUNCT_2, FCONT_1, FDIFF_1, LIMFUNC1, LIMFUNC2, LIMFUNC3, PARTFUN1,
      MEMBERED, XBOOLE_0;
 clusters FCONT_3, RELSET_1, XREAL_0, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin

 reserve f,g for PartFunc of REAL,REAL,
         r,r1,r2,g1,g2,g3,g4,g5,g6,x,x0,t,c for Real,
         a,b,s for Real_Sequence,
         n,k for Nat;

theorem :: L_HOSPIT:1
  f is_continuous_in x0 &
(for r1,r2 st r1<x0 & x0<r2
  ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f &
  g2<r2 & x0<g2 & g2 in dom f) implies
f is_convergent_in x0;

theorem :: L_HOSPIT:2
f is_right_convergent_in x0 & lim_right(f,x0) = t iff
(for r st x0<r ex t st t<r & x0<t & t in dom f) &
for a 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;

theorem :: L_HOSPIT:3
f is_left_convergent_in x0 & lim_left(f,x0) = t iff
(for r st r<x0 ex t st r<t & t<x0 & t in dom f) &
for a 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;

theorem :: L_HOSPIT:4
(ex N being Neighbourhood of x0 st N\{x0} c=dom f) implies
(for r1,r2 st r1<x0 & x0<r2
  ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f);

theorem :: L_HOSPIT:5
  (ex N being Neighbourhood of x0 st 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)
implies f/g is_divergent_to+infty_in x0;

theorem :: L_HOSPIT:6
  (ex N being Neighbourhood of x0 st 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)
implies f/g is_divergent_to-infty_in x0;

theorem :: L_HOSPIT:7
  (ex r st r>0 & 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) implies
f/g is_right_convergent_in x0 & ex r st r>0 &
lim_right(f/g,x0) = lim_right(((f`|(].x0,x0+r.[))/(g`|(].x0,x0+r.[))),x0);

theorem :: L_HOSPIT:8
  (ex r st r>0 & 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) implies
f/g is_left_convergent_in x0 & ex r st r>0 &
lim_left(f/g,x0) = lim_left(((f`|(].x0-r,x0.[))/(g`|(].x0-r,x0.[))),x0);

theorem :: L_HOSPIT:9
  (ex N being Neighbourhood of x0 st 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) implies
f/g is_convergent_in x0 &
(ex N being Neighbourhood of x0 st lim(f/g,x0) = lim(((f`|N)/(g`|N)),x0));

theorem :: L_HOSPIT:10
  (ex N being Neighbourhood of x0 st 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)
implies f/g is_convergent_in x0 & lim(f/g,x0) = diff(f,x0)/diff(g,x0);