The abstract of the Mizar article:

Average Value Theorems for Real Functions of One Variable

by

Jaroslaw Kotowicz,

Konrad Raczkowski, and

Pawel Sadowski

Received June 18, 1990

MML identifier: ROLLE

[ Mizar article, MML identifier index ]

environ

 vocabulary SEQ_1, PARTFUN1, FCONT_1, RCOMP_1, FUNCT_1, FDIFF_1, PRE_TOPC,
      RELAT_1, COMPTS_1, ARYTM, SEQ_4, LATTICES, SEQ_2, PARTFUN2, ARYTM_3,
      BOOLE, ARYTM_1, SEQM_3, ORDINAL2, RFUNCT_2;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, RELSET_1, SEQ_1, SEQ_2, SEQM_3, SEQ_4, PARTFUN1, PARTFUN2,
      RFUNCT_2, RCOMP_1, FCONT_1, FDIFF_1;
 constructors REAL_1, SEQ_2, SEQM_3, SEQ_4, PARTFUN2, RFUNCT_2, RCOMP_1,
      FCONT_1, FDIFF_1, PARTFUN1, MEMBERED, XBOOLE_0;
 clusters RCOMP_1, FDIFF_1, RELSET_1, XREAL_0, SEQ_1, NAT_1, MEMBERED,
      ZFMISC_1, XBOOLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve y for set;
reserve g,r,s,p,t,x,x0,x1,x2 for Real;
reserve n,n1 for Nat;
reserve s1,s2,s3 for Real_Sequence;
reserve f,f1,f2,f3 for PartFunc of REAL,REAL;

theorem :: ROLLE:1
for p,g st p<g for f st
f is_continuous_on [.p,g.] & f.p=f.g & f is_differentiable_on ].p,g.[
ex x0 st x0 in ].p,g.[ & diff(f,x0)=0;

theorem :: ROLLE:2
  for x,t st 0<t for f st f is_continuous_on [.x,x+t.] &
f.x=f.(x+t) & f is_differentiable_on ].x,x+t.[
ex s st 0<s & s<1 & diff(f,x+s*t)=0;

theorem :: ROLLE:3
for p,g st p<g for f st
f is_continuous_on [.p,g.] & f is_differentiable_on ].p,g.[
ex x0 st x0 in ].p,g.[ & diff(f,x0)=(f.g-f.p)/(g-p);

theorem :: ROLLE:4
  for x,t st 0<t for f st f is_continuous_on [.x,x+t.] &
f is_differentiable_on ].x,x+t.[
ex s st 0<s & s<1 & f.(x+t) = f.x + t*diff(f,x+s*t);

theorem :: ROLLE:5
for p,g st p<g for f1,f2 st
f1 is_continuous_on [.p,g.] & f1 is_differentiable_on ].p,g.[ &
f2 is_continuous_on [.p,g.] & f2 is_differentiable_on ].p,g.[
ex x0 st x0 in ].p,g.[ & (f1.g-f1.p)*diff(f2,x0)=(f2.g-f2.p)*diff(f1,x0);

theorem :: ROLLE:6
  for x,t st 0<t for f1,f2 st f1 is_continuous_on [.x,x+t.] &
f1 is_differentiable_on ].x,x+t.[ & f2 is_continuous_on [.x,x+t.] &
f2 is_differentiable_on ].x,x+t.[ &
(for x1 st x1 in ].x,x+t.[ holds diff(f2,x1)<>0)
ex s st 0<s & s<1 &
(f1.(x+t)-f1.x)/(f2.(x+t)-f2.x) = diff(f1,x+s*t)/diff(f2,x+s*t);

theorem :: ROLLE:7
for p,g st p<g for f st f is_differentiable_on ].p,g.[ &
(for x st x in ].p,g.[ holds diff(f,x) = 0)
holds f is_constant_on ].p,g.[;

theorem :: ROLLE:8
  for p,g st p<g for f1,f2 st f1 is_differentiable_on ].p,g.[ &
f2 is_differentiable_on ].p,g.[ &
(for x st x in ].p,g.[ holds diff(f1,x) = diff(f2,x))
holds f1-f2 is_constant_on ].p,g.[ &
ex r st for x st x in ].p,g.[ holds f1.x = f2.x+r;

theorem :: ROLLE:9
  for p,g st p<g for f st f is_differentiable_on ].p,g.[ &
(for x st x in ].p,g.[ holds 0<diff(f,x))
holds f is_increasing_on ].p,g.[;

theorem :: ROLLE:10
  for p,g st p<g for f st f is_differentiable_on ].p,g.[ &
(for x st x in ].p,g.[ holds diff(f,x)<0)
holds f is_decreasing_on ].p,g.[;

theorem :: ROLLE:11
  for p,g st p<g for f st f is_differentiable_on ].p,g.[ &
(for x st x in ].p,g.[ holds 0<=diff(f,x))
holds f is_non_decreasing_on ].p,g.[;

theorem :: ROLLE:12
  for p,g st p<g for f st f is_differentiable_on ].p,g.[ &
(for x st x in ].p,g.[ holds diff(f,x)<=0)
holds f is_non_increasing_on ].p,g.[;