:: Average Value Theorems for Real Functions of One Variable
:: by Jaros{\l}aw Kotowicz, Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, SUBSET_1, SEQ_1, PARTFUN1, ARYTM_3, XXREAL_1,
TARSKI, RELAT_1, ORDINAL2, FUNCT_1, FDIFF_1, CARD_1, RCOMP_1, XXREAL_2,
SEQ_4, XXREAL_0, XBOOLE_0, ARYTM_1, VALUED_0, SEQ_2, VALUED_1, FUNCT_2,
FUNCOP_1, FUNCT_7, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_1, FUNCT_2, NUMBERS,
XREAL_0, XXREAL_0, XXREAL_2, XCMPLX_0, REAL_1, RELSET_1, VALUED_0,
VALUED_1, SEQ_1, SEQ_2, SEQ_4, PARTFUN1, PARTFUN2, RCOMP_1, FCONT_1,
FDIFF_1;
constructors PARTFUN1, REAL_1, NAT_1, SEQ_2, SEQ_4, RCOMP_1, PARTFUN2,
RFUNCT_2, FCONT_1, FDIFF_1, VALUED_1, XXREAL_2, COMPLEX1, RELSET_1,
BINOP_2, COMSEQ_2;
registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, RCOMP_1,
FDIFF_1, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, FCONT_1, ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities XCMPLX_0;
expansions TARSKI;
theorems TARSKI, NAT_1, SEQ_1, SEQ_2, SEQ_4, PARTFUN2, RFUNCT_2, RCOMP_1,
FCONT_1, FDIFF_1, ZFMISC_1, FUNCT_1, XREAL_0, XBOOLE_0, XBOOLE_1,
XCMPLX_1, FUNCOP_1, XREAL_1, XXREAL_0, VALUED_1, XXREAL_2, XXREAL_1,
FUNCT_2, VALUED_0, ORDINAL1;
schemes SEQ_1;
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 for PartFunc of REAL,REAL;
theorem Th1:
for p,g st p<g for f st [.p,g.] c= dom f & f|[.p,g.] is
continuous & f.p=f.g & f is_differentiable_on ].p,g.[ ex x0 st x0 in ].p,g.[ &
diff(f,x0)=0
proof
let p,g such that
A1: p<g;
reconsider Z=].p,g.[ as open Subset of REAL;
let f such that
A2: [.p,g.] c= dom f and
A3: f|[.p,g.] is continuous and
A4: f.p=f.g and
A5: f is_differentiable_on ].p,g.[;
A6: f.:[.p,g.] is compact by A2,A3,FCONT_1:29,RCOMP_1:6;
[.p,g.] is compact by RCOMP_1:6;
then
A7: f.:[.p,g.] is real-bounded by A2,A3,FCONT_1:29,RCOMP_1:10;
p in [.p,g.] by A1,XXREAL_1:1;
then consider x1,x2 be Real such that
A8: x1 in [.p,g.] and
A9: x2 in [.p,g.] and
A10: f.x1 = upper_bound (f.:[.p,g.]) and
A11: f.x2 = lower_bound (f.:[.p,g.]) by A2,A3,FCONT_1:31,RCOMP_1:6;
reconsider x1,x2 as Element of REAL by XREAL_0:def 1;
p in {r: p<=r & r<=g} by A1;
then p in [.p,g.] by RCOMP_1:def 1;
then f.p in f.:[.p,g.] by A2,FUNCT_1:def 6;
then
A12: not f.x1 < f.x2 by A10,A11,A6,RCOMP_1:10,SEQ_4:11;
A13: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
then
A14: ].p,g.[ c= dom f by A2;
per cases by A12,XXREAL_0:1;
suppose
A15: f.x1 = f.x2;
p/2<g/2 by A1,XREAL_1:74;
then p/2+g/2<g/2+g/2 & p/2+p /2<p/2+g/2 by XREAL_1:8;
then p/2+g/2 in {r: p<r & r<g};
then
A16: p/2+g/2 in Z by RCOMP_1:def 2;
f|[.p,g.] is constant by A10,A11,A7,A15,RFUNCT_2:19;
then f|Z is constant by PARTFUN2:38,XXREAL_1:25;
then (f`|Z).(p/2+g/2) = 0 by A14,A16,FDIFF_1:22;
then diff(f,(p/2+g/2)) = 0 by A5,A16,FDIFF_1:def 7;
hence thesis by A16;
end;
suppose
A17: f.x2 < f.x1;
A18: x2 in ].p,g.[ or x1 in ].p,g.[
proof
assume that
A19: not x2 in ].p,g.[ and
A20: not x1 in ].p,g.[;
x1 in ].p,g.[ \/ {p,g} by A1,A8,XXREAL_1:128;
then x1 in {p,g} by A20,XBOOLE_0:def 3;
then
A21: x1 = p or x1 = g by TARSKI:def 2;
x2 in ].p,g.[ \/ {p,g} by A1,A9,XXREAL_1:128;
then x2 in {p,g} by A19,XBOOLE_0:def 3;
hence contradiction by A4,A17,A21,TARSKI:def 2;
end;
now
per cases by A18;
case
A22: x2 in ].p,g.[;
then consider N1 be Neighbourhood of x2 such that
A23: N1 c= Z by RCOMP_1:18;
consider r be Real such that
A24: 0<r and
A25: N1=].x2-r,x2+r.[ by RCOMP_1:def 6;
reconsider r as Real;
deffunc F(Nat)=r/($1+2);
consider s2 such that
A26: for n holds s2.n=F(n) from SEQ_1:sch 1;
now
let n;
0<>r/(n+2) by A24,XREAL_1:139;
hence 0<>s2.n by A26;
end;
then
A27: s2 is non-zero by SEQ_1:5;
s2 is convergent & lim s2 = 0 by A26,SEQ_4:31;
then reconsider h1 = s2 as 0-convergent non-zero Real_Sequence by A27,
FDIFF_1:def 1;
consider s1 such that
A28: rng s1 = {x2} by SEQ_1:6;
reconsider c = s1 as constant Real_Sequence by A28,FUNCT_2:111;
A29: now
let n;
c.n in {x2} by A28,VALUED_0:28;
hence c.n = x2 by TARSKI:def 1;
end;
deffunc G(Nat) = -(r/($1+2));
consider s3 such that
A30: for n holds s3.n=G(n) from SEQ_1:sch 1;
now
let n;
s3.n = -(r/(n+2)) by A30;
hence s3.n = (-r)/(n+2);
end;
then
A31: s3 is convergent & lim s3 = 0 by SEQ_4:31;
now
let n;
-0<>-(r/(n+2)) by A24,XREAL_1:139;
hence 0<>s3.n by A30;
end;
then s3 is non-zero by SEQ_1:5;
then reconsider h2 = s3 as 0-convergent non-zero Real_Sequence by A31,
FDIFF_1:def 1;
A32: N1 c= dom f by A14,A23;
A33: now
let n;
0+1<=n+1 by XREAL_1:6;
then 1<n+1+1 by NAT_1:13;
then r/(n+2)<r/1 by A24,XREAL_1:76;
then
A34: x2 - r < x2 - r/(n+2) by XREAL_1:15;
x2-r/(n+2)<x2+r by A24,XREAL_1:6;
then x2-r/(n+2) in {s: x2-r<s & s<x2+r} by A34;
hence x2-r/(n+2) in N1 by A25,RCOMP_1:def 2;
end;
A35: rng (h2+c) c= N1
proof
let y be object;
assume y in rng (h2+c);
then consider n being Element of NAT such that
A36: (h2+c).n=y by FUNCT_2:113;
y = h2.n + c.n by A36,SEQ_1:7
.= -(r/(n+2)) + c.n by A30
.= x2 - r/(n+2) by A29;
hence thesis by A33;
end;
A37: now
let n;
0+1<=n+1 by XREAL_1:6;
then 1<n+1+1 by NAT_1:13;
then r/(n+2)<r/1 by A24,XREAL_1:76;
then
A38: x2 + r/(n+2) < x2 + r by XREAL_1:6;
0< r/(n+2) by A24,XREAL_1:139;
then x2-r<x2+r/(n+2) by A24,XREAL_1:6;
then x2+r/(n+2) in {s: x2-r<s & s<x2+r} by A38;
hence x2+r/(n+2) in N1 by A25,RCOMP_1:def 2;
end;
A39: rng (h1+c) c= N1
proof
let y be object;
assume y in rng (h1+c);
then consider n being Element of NAT such that
A40: (h1+c).n=y by FUNCT_2:113;
y = h1.n + c.n by A40,SEQ_1:7
.= r/(n+2) + c.n by A26
.= x2 + r/(n+2) by A29;
hence thesis by A37;
end;
A41: now
let n;
0<r/(n+2) by A24,XREAL_1:139;
hence 0<s2.n by A26;
end;
A42: for n holds 0<=(h1"(#)(f/*(h1+c) - f/*c)).n
proof
let n;
A43: 0<h1.n & (h1").n = (h1.n)" by A41,VALUED_1:10;
(h1+c).n in rng(h1+c) by VALUED_0:28;
then (h1+c).n in N1 by A39;
then (h1+c).n in Z by A23;
then f.((h1+c).n) in f.:[.p,g.] by A13,A14,FUNCT_1:def 6;
then f.x2 <= f.((h1+c).n) by A11,A7,SEQ_4:def 2;
then
A44: 0<=f.((h1+c).n) - f.x2 by XREAL_1:48;
reconsider n as Element of NAT by ORDINAL1:def 12;
now
let n1 be Element of NAT;
(h1+c).n1 in rng(h1+c) by VALUED_0:28;
then (h1+c).n1 in N1 by A39;
hence (h1+c).n1 in ].p,g.[ by A23;
end;
then
A45: rng (h1+c) c= ].p,g.[ by FUNCT_2:114;
A46: rng c c= dom f by A2,A9,A28,ZFMISC_1:31;
(h1"(#)(f/*(h1+c) - f/*c)).n = (h1").n*(f/*(h1+c) - f/*c).n by
SEQ_1:8
.= (h1").n*((f/*(h1+c)).n - (f/*c).n) by RFUNCT_2:1
.= (h1").n*(f.((h1+c).n) - (f/*c).n) by A14,A45,FUNCT_2:108
,XBOOLE_1:1
.= (h1").n*(f.((h1+c).n) - f.(c.n)) by A46,FUNCT_2:108
.= (h1").n*(f.((h1+c).n) - f.x2) by A29;
hence thesis by A44,A43;
end;
A47: f is_differentiable_in x2 by A5,A22,FDIFF_1:9;
then
h1"(#)(f/*(h1+c) - f/*c) is convergent & diff(f,x2) = lim (h1"(#)
(f/*(h1+c) - f/*c)) by A32,A28,A39,FDIFF_1:12;
then
A48: 0 <= diff(f,x2) by A42,SEQ_2:17;
A49: now
let n;
0<r/(n+2) by A24,XREAL_1:139;
then -(r/(n+2))<-0 by XREAL_1:24;
hence s3.n<0 by A30;
end;
A50: for n holds (h2"(#)(f/*(h2+c) - f/*c)).n <= 0
proof
let n;
now
let n1 be Element of NAT;
(h2+c).n1 in rng(h2+c) by VALUED_0:28;
then (h2+c).n1 in N1 by A35;
hence (h2+c).n1 in ].p,g.[ by A23;
end;
then
A51: rng (h2+c) c= ].p,g.[ by FUNCT_2:114;
h2.n<0 by A49;
then -0<-h2.n by XREAL_1:24;
then 0<1/(-h2.n);
then (h2").n = (h2.n)" & 0<-1/(h2.n) by VALUED_1:10,XCMPLX_1:188;
then
A52: (h2").n<=0;
(h2+c).n in rng(h2+c) by VALUED_0:28;
then (h2+c).n in N1 by A35;
then (h2+c).n in Z by A23;
then f.((h2+c).n) in f.:[.p,g.] by A13,A14,FUNCT_1:def 6;
then f.x2 <= f.((h2+c).n) by A11,A7,SEQ_4:def 2;
then
A53: 0<=f.((h2+c).n)-f.x2 by XREAL_1:48;
reconsider n as Element of NAT by ORDINAL1:def 12;
A54: rng c c= dom f by A2,A9,A28,ZFMISC_1:31;
(h2"(#)(f/*(h2+c) - f/*c)).n = (h2").n*(f/*(h2+c) - f/*c).n by
SEQ_1:8
.= (h2").n*((f/*(h2+c)).n - (f/*c).n) by RFUNCT_2:1
.= (h2").n*(f.((h2+c).n) - (f/*c).n) by A14,A51,FUNCT_2:108
,XBOOLE_1:1
.= (h2").n*(f.((h2+c).n) - f.(c.n)) by A54,FUNCT_2:108
.= (h2").n*(f.((h2+c).n) - f.(x2)) by A29;
hence thesis by A53,A52;
end;
h2"(#)(f/*(h2+c) - f/*c) is convergent & diff(f,x2) = lim (h2"(#)
(f/*(h2+c) - f/*c)) by A47,A32,A28,A35,FDIFF_1:12;
hence x2 in ].p,g.[ & diff(f,x2) = 0 by A22,A48,A50,RFUNCT_2:7;
end;
case
A55: x1 in ].p,g.[;
then consider N1 be Neighbourhood of x1 such that
A56: N1 c= ].p,g.[ by RCOMP_1:18;
consider r be Real such that
A57: 0<r and
A58: N1=].x1-r,x1+r.[ by RCOMP_1:def 6;
reconsider r as Real;
deffunc F(Nat) = r/($1+2);
consider s2 such that
A59: for n holds s2.n=F(n) from SEQ_1:sch 1;
now
let n;
0<>r/(n+2) by A57,XREAL_1:139;
hence 0<>s2.n by A59;
end;
then
A60: s2 is non-zero by SEQ_1:5;
s2 is convergent & lim s2 = 0 by A59,SEQ_4:31;
then reconsider h1 = s2 as 0-convergent non-zero Real_Sequence by A60,
FDIFF_1:def 1;
consider s1 such that
A61: rng s1 = {x1} by SEQ_1:6;
reconsider c = s1 as constant Real_Sequence by A61,FUNCT_2:111;
A62: now
let n;
c.n in {x1} by A61,VALUED_0:28;
hence c.n = x1 by TARSKI:def 1;
end;
deffunc G(Nat) = -(r/($1+2));
consider s3 such that
A63: for n holds s3.n=G(n) from SEQ_1:sch 1;
now
let n;
s3.n = -(r/(n+2)) by A63;
hence s3.n = (-r)/(n+2);
end;
then
A64: s3 is convergent & lim s3 = 0 by SEQ_4:31;
now
let n;
-0<>-(r/(n+2)) by A57,XREAL_1:139;
hence 0<>s3.n by A63;
end;
then s3 is non-zero by SEQ_1:5;
then reconsider h2 = s3 as 0-convergent non-zero Real_Sequence by A64,
FDIFF_1:def 1;
A65: N1 c= dom f by A14,A56;
A66: now
let n;
0+1<=n+1 by XREAL_1:6;
then 1<n+1+1 by NAT_1:13;
then r/(n+2)<r/1 by A57,XREAL_1:76;
then
A67: x1 - r < x1 - r/(n+2) by XREAL_1:15;
x1-r/(n+2)<x1+r by A57,XREAL_1:6;
then x1-r/(n+2) in {s: x1-r<s & s<x1+r} by A67;
hence x1-r/(n+2) in N1 by A58,RCOMP_1:def 2;
end;
A68: rng (h2+c) c= N1
proof
let y be object;
assume y in rng (h2+c);
then consider n being Element of NAT such that
A69: (h2+c).n=y by FUNCT_2:113;
y = h2.n + c.n by A69,SEQ_1:7
.= -r/(n+2) + c.n by A63
.= x1 - r/(n+2) by A62;
hence thesis by A66;
end;
A70: now
let n;
0+1<=n+1 by XREAL_1:6;
then 1<n+1+1 by NAT_1:13;
then r/(n+2)<r/1 by A57,XREAL_1:76;
then
A71: x1 + r/(n+2) < x1 + r by XREAL_1:6;
0< r/(n+2) by A57,XREAL_1:139;
then x1-r<x1+r/(n+2) by A57,XREAL_1:6;
then x1+r/(n+2) in {s: x1-r<s & s<x1+r} by A71;
hence x1+r/(n+2) in N1 by A58,RCOMP_1:def 2;
end;
A72: rng (h1+c) c= N1
proof
let y be object;
assume y in rng (h1+c);
then consider n being Element of NAT such that
A73: (h1+c).n=y by FUNCT_2:113;
y = h1.n + c.n by A73,SEQ_1:7
.= r/(n+2) + c.n by A59
.= x1 + r/(n+2) by A62;
hence thesis by A70;
end;
A74: now
let n;
0<r/(n+2) by A57,XREAL_1:139;
hence 0<s2.n by A59;
end;
A75: for n holds (h1"(#)(f/*(h1+c) - f/*c)).n <= 0
proof
let n;
A76: 0<h1.n & (h1").n = (h1.n)" by A74,VALUED_1:10;
(h1+c).n in rng(h1+c) by VALUED_0:28;
then (h1+c).n in N1 by A72;
then (h1+c).n in Z by A56;
then f.((h1+c).n) in f.:[.p,g.] by A13,A14,FUNCT_1:def 6;
then f.((h1+c).n) <= f.x1 by A10,A7,SEQ_4:def 1;
then 0<=f.x1 - f.((h1+c).n) by XREAL_1:48;
then
A77: -(f.x1 - f.((h1+c).n))<=-0;
now
let n1 be Element of NAT ;
(h1+c).n1 in rng(h1+c) by VALUED_0:28;
then (h1+c).n1 in N1 by A72;
hence (h1+c).n1 in ].p,g.[ by A56;
end;
then
A78: rng (h1+c) c= ].p,g.[ by FUNCT_2:114;
reconsider n as Element of NAT by ORDINAL1:def 12;
A79: rng c c= dom f by A2,A8,A61,ZFMISC_1:31;
(h1"(#)(f/*(h1+c) - f/*c)).n = (h1").n*(f/*(h1+c) - f/*c).n by
SEQ_1:8
.= (h1").n*((f/*(h1+c)).n - (f/*c).n) by RFUNCT_2:1
.= (h1").n*(f.((h1+c).n) - (f/*c).n) by A14,A78,FUNCT_2:108
,XBOOLE_1:1
.= (h1").n*(f.((h1+c).n) - f.(c.n)) by A79,FUNCT_2:108
.= (h1").n*(f.((h1+c).n) - f.x1) by A62;
hence thesis by A77,A76;
end;
A80: f is_differentiable_in x1 by A5,A55,FDIFF_1:9;
then h1"(#)(f/*(h1+c) - f/*c) is convergent & diff(f,x1) = lim (h1"
(#)(f/*(h1+c) - f/*c)) by A65,A61,A72,FDIFF_1:12;
then
A81: diff(f,x1) <= 0 by A75,RFUNCT_2:7;
A82: now
let n;
0<r/(n+2) by A57,XREAL_1:139;
then -(r/(n+2))<-0 by XREAL_1:24;
hence s3.n<0 by A63;
end;
A83: for n holds 0 <= (h2"(#)(f/*(h2+c) - f/*c)).n
proof
let n;
now
let n1 be Element of NAT ;
(h2+c).n1 in rng(h2+c) by VALUED_0:28;
then (h2+c).n1 in N1 by A68;
hence (h2+c).n1 in ].p,g.[ by A56;
end;
then
A84: rng (h2+c) c= ].p,g.[ by FUNCT_2:114;
h2.n<0 by A82;
then -0<-h2.n by XREAL_1:24;
then 0<1/(-h2.n);
then (h2").n = (h2.n)" & 0<-1/(h2.n) by VALUED_1:10,XCMPLX_1:188;
then
A85: (h2").n<=0;
reconsider n as Element of NAT by ORDINAL1:def 12;
(h2+c).n in rng(h2+c) by VALUED_0:28;
then (h2+c).n in N1 by A68;
then (h2+c).n in Z by A56;
then f.((h2+c).n) in f.:[.p,g.] by A13,A14,FUNCT_1:def 6;
then f.((h2+c).n) <= f.x1 by A10,A7,SEQ_4:def 1;
then 0<=f.x1 - f.((h2+c).n) by XREAL_1:48;
then
A86: -(f.x1 - f.((h2+c).n))<=-0;
A87: rng c c= dom f by A2,A8,A61,ZFMISC_1:31;
(h2"(#)(f/*(h2+c) - f/*c)).n = (h2").n*(f/*(h2+c) - f/*c).n by
SEQ_1:8
.= (h2").n*((f/*(h2+c)).n - (f/*c).n) by RFUNCT_2:1
.= (h2").n*(f.((h2+c).n) - (f/*c).n) by A14,A84,FUNCT_2:108
,XBOOLE_1:1
.= (h2").n*(f.((h2+c).n) - f.(c.n)) by A87,FUNCT_2:108
.= (h2").n*(f.((h2+c).n) - f.(x1)) by A62;
hence thesis by A86,A85;
end;
h2"(#)(f/*(h2+c) - f/*c) is convergent & diff(f,x1) = lim (h2"
(#)(f/*(h2+c) - f/*c)) by A80,A65,A61,A68,FDIFF_1:12;
hence x1 in ].p,g.[ & diff(f,x1) = 0 by A55,A81,A83,SEQ_2:17;
end;
end;
hence thesis;
end;
end;
::$N Rolle Theorem
theorem
for x,t st 0<t for f st [.x,x+t.] c= dom f & f|[.x,x+t.] is continuous
& 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
proof
let x,t such that
A1: 0<t;
let f;
assume [.x,x+t.] c= dom f & f|[.x,x+t.] is continuous & f.x=f.(x+t) & f
is_differentiable_on ].x,x+t.[;
then consider x0 such that
A2: x0 in ].x,x+t.[ and
A3: diff(f,x0)=0 by A1,Th1,XREAL_1:29;
take s = (x0-x)/t;
x0 in {r: x<r & r<x+t} by A2,RCOMP_1:def 2;
then
A4: ex g st g=x0 & x<g & g<x+t;
then 0<x0-x by XREAL_1:50;
then 0/t < (x0-x)/t by A1,XREAL_1:74;
hence 0<s;
x0-x<t by A4,XREAL_1:19;
then (x0-x)/t<t/t by A1,XREAL_1:74;
hence s<1 by A1,XCMPLX_1:60;
s*t+x = (x0-x)+x by A1,XCMPLX_1:87;
hence thesis by A3;
end;
::$N The Mean Value Theorem
::$L https://en.wikipedia.org/wiki/Mean_value_theorem The Mean Value Theorem
theorem Th3:
for p,g st p<g for f st [.p,g.] c= dom f & f|[.p,g.] is
continuous & f is_differentiable_on ].p,g.[ ex x0 st x0 in ].p,g.[ & diff(f,x0)
=(f.g-f.p)/(g-p)
proof
let p,g such that
A1: p<g;
A2: 0<>g-p by A1;
reconsider Z=].p,g.[ as open Subset of REAL;
defpred P[set] means $1 in [.p,g.];
let f such that
A3: [.p,g.] c= dom f and
A4: f|[.p,g.] is continuous and
A5: f is_differentiable_on ].p,g.[;
set r = (f.g-f.p)/(g-p);
deffunc F(Real) =In(r*($1-p),REAL);
consider f1 such that
A6: (for x being Element of REAL holds x in dom f1 iff P[x]) &
for x being Element of REAL st x in dom f1 holds f1.x = F(x)
from SEQ_1:sch 3;
A7: for x being Real st x in dom f1 holds f1.x = r*(x-p)
proof let x be Real such that
A8: x in dom f1;
reconsider x as Real;
f1.x = F(x) by A6,A8;
hence thesis;
end;
set f2 = f - f1;
A9: [.p,g.] c= dom f1
by A6;
then
A10: [.p,g.] c= dom f /\ dom f1 by A3,XBOOLE_1:19;
then
A11: [.p,g.] c= dom f2 by VALUED_1:12;
[.p,g.] = ].p,g.[ \/ {p,g} by A1,XXREAL_1:128;
then
A12: {p,g} c= [.p,g.] by XBOOLE_1:7;
then
A13: p in [.p,g.] by ZFMISC_1:32;
then
A14: p in dom f1 by A6;
[.p,g.] c= dom f /\ dom f1 by A3,A9,XBOOLE_1:19;
then
A15: [.p,g.] c= dom f2 by VALUED_1:12;
then
A16: f2.p = f.p-f1.p by A13,VALUED_1:13
.= f.p - r*(p-p) by A14,A7
.= f.p;
A17: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
then
A18: Z c= dom f1 by A9;
A19: now
let x;
assume x in Z;
then x in dom f1 by A17,A6;
hence f1.x = r*(x-p) by A7
.= r*x + -r*p;
end;
then
A20: f1 is_differentiable_on Z by A18,FDIFF_1:23;
now
let x be Real;
assume x in [.p,g.];
then x in dom f1 by A6;
hence f1.x = r*(x-p) by A7
.= r*x + -r*p;
end;
then f1|[.p,g.] is continuous by FCONT_1:41;
then
A21: f2|[.p,g.] is continuous by A4,A10,FCONT_1:18;
A22: g in [.p,g.] by A12,ZFMISC_1:32;
then
A23: g in dom f1 by A6;
Z c= dom f by A3,A17;
then Z c= dom f /\ dom f1 by A18,XBOOLE_1:19;
then
A24: Z c= dom f2 by VALUED_1:12;
f2.g = f.g-f1.g by A22,A15,VALUED_1:13
.= f.g - ((f.g-f.p)/(g-p))*(g-p) by A7,A23
.= f.g - (f.g-f.p) by A2,XCMPLX_1:87
.= f2.p by A16;
then consider x0 such that
A25: x0 in ].p,g.[ and
A26: diff(f2,x0)=0 by A1,A5,A20,A11,A21,A24,Th1,FDIFF_1:19;
take x0;
f2 is_differentiable_on Z by A5,A20,A24,FDIFF_1:19;
then diff(f2,x0) = (f2`|Z).x0 by A25,FDIFF_1:def 7
.= diff(f,x0) - diff(f1,x0) by A5,A20,A24,A25,FDIFF_1:19
.= diff(f,x0) - (f1`|Z).x0 by A20,A25,FDIFF_1:def 7;
hence thesis by A18,A19,A25,A26,FDIFF_1:23;
end;
::$N Lagrange Theorem
theorem
for x,t st 0<t for f st [.x,x+t.] c= dom f & f|[.x,x+t.] is continuous
& 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)
proof
let x,t such that
A1: 0<t;
let f;
assume [.x,x+t.] c= dom f & f|[.x,x+t.] is continuous & f
is_differentiable_on ].x,x+t.[;
then consider x0 such that
A2: x0 in ].x,x+t.[ and
A3: diff(f,x0)=(f.(x+t)-f.x)/(x+t-x) by A1,Th3,XREAL_1:29;
take s = (x0-x)/t;
x0 in {r: x<r & r<x+t} by A2,RCOMP_1:def 2;
then
A4: ex g st g=x0 & x<g & g<x+t;
then 0<x0-x by XREAL_1:50;
then 0/t < (x0-x)/t by A1,XREAL_1:74;
hence 0<s;
x0-x<t by A4,XREAL_1:19;
then (x0-x)/t<t/t by A1,XREAL_1:74;
hence s<1 by A1,XCMPLX_1:60;
A5: s*t+x = (x0-x)+x by A1,XCMPLX_1:87;
f.x + t*diff(f,x0)=f.x + (f.(x+t)-f.x) by A1,A3,XCMPLX_1:87;
hence thesis by A5;
end;
theorem Th5:
for p,g st p<g for f1,f2 st [.p,g.] c= dom f1 & [.p,g.] c= dom f2
& f1|[.p,g.] is continuous & f1 is_differentiable_on ].p,g.[ & f2|[.p,g.] is
continuous & 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)
proof
let p,g such that
A1: p<g;
let f1,f2 such that
A2: [.p,g.] c= dom f1 and
A3: [.p,g.] c= dom f2 and
A4: f1|[.p,g.] is continuous and
A5: f1 is_differentiable_on ].p,g.[ and
A6: f2|[.p,g.] is continuous and
A7: f2 is_differentiable_on ].p,g.[;
A8: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
now
per cases;
suppose
A9: f2.p=f2.g;
then consider x0 such that
A10: x0 in ].p,g.[ & diff(f2,x0) = 0 by A1,A3,A6,A7,Th1;
take x0;
thus x0 in ].p,g.[ & (f1.g-f1.p)*diff(f2,x0)=(f2.g-f2.p)*diff(f1,x0) by
A9,A10;
end;
suppose
f2.p<>f2.g;
then
A11: f2.g-f2.p<>0;
reconsider Z=].p,g.[ as open Subset of REAL;
set s=(f1.g-f1.p)/(f2.g-f2.p);
reconsider fp = f1.p - f2.p*s as Element of REAL by XREAL_0:def 1;
reconsider f3 = [.p,g.] --> fp as PartFunc of [.p,g.], REAL
by FUNCOP_1:45;
reconsider f3 as PartFunc of REAL, REAL;
set f4 = s(#)f2;
set f5 = f3+f4;
set f=f5-f1;
A12: Z c= dom f3 by A8,FUNCOP_1:13;
A13: dom f4 = dom f2 by VALUED_1:def 5;
then
A14: Z c= dom f4 by A3,A8;
then Z c= dom f3 /\ dom f4 by A12,XBOOLE_1:19;
then
A15: Z c= dom f5 by VALUED_1:def 1;
reconsider f1pf2p =f1.p - f2.p*s as Element of REAL by XREAL_0:def 1;
A16: [.p,g.] = dom f3 by FUNCOP_1:13;
then for x being Element of REAL st x in [.p,g.] /\ dom f3
holds f3.x=f1pf2p by FUNCOP_1:7;
then
A17: f3|[.p,g.] is constant by PARTFUN2:57;
then
A18: f3|].p,g.[ is constant by PARTFUN2:38,XXREAL_1:25;
then
A19: f3 is_differentiable_on Z by A12,FDIFF_1:22;
A20: p in [.p,g.] by A1,XXREAL_1:1;
then p in dom f3 /\ dom f4 by A3,A16,A13,XBOOLE_0:def 4;
then
A21: p in dom f5 by VALUED_1:def 1;
then p in dom f5 /\ dom f1 by A2,A20,XBOOLE_0:def 4;
then p in dom f by VALUED_1:12;
then
A22: f.p = f5.p - f1.p by VALUED_1:13
.= f3.p + f4.p - f1.p by A21,VALUED_1:def 1
.= f3.p + s*f2.p - f1.p by A3,A13,A20,VALUED_1:def 5
.= f1.p - s*f2.p + s*f2.p - f1.p by A20,FUNCOP_1:7
.= 0;
A23: g in [.p,g.] by A1,XXREAL_1:1;
then g in dom f3 /\ dom f4 by A3,A16,A13,XBOOLE_0:def 4;
then
A24: g in dom f5 by VALUED_1:def 1;
then g in dom f5 /\ dom f1 by A2,A23,XBOOLE_0:def 4;
then g in dom f by VALUED_1:12;
then
A25: f.g = f5.g - f1.g by VALUED_1:13
.= f3.g + f4.g - f1.g by A24,VALUED_1:def 1
.= f3.g + s*f2.g - f1.g by A3,A13,A23,VALUED_1:def 5
.= f1.p - s*f2.p + s*f2.g - f1.g by A23,FUNCOP_1:7
.= -f1.g+(f1.p-(-(f1.g-f1.p))/(f2.g-f2.p)*(f2.g-f2.p))
.= -f1.g+(f1.p-(f1.p-f1.g)) by A11,XCMPLX_1:87
.= f.p by A22;
Z c= dom f1 by A2,A8;
then Z c= dom f5 /\ dom f1 by A15,XBOOLE_1:19;
then
A26: Z c= dom f by VALUED_1:12;
dom f4 = dom f2 by VALUED_1:def 5;
then
A27: [.p,g.] c= dom f3 /\ dom f4 by A3,A16,XBOOLE_1:19;
then [.p,g.] c= dom f5 by VALUED_1:def 1;
then
A28: [.p,g.] c= dom f5 /\ dom f1 by A2,XBOOLE_1:19;
f4|[.p,g.] is continuous by A3,A6,FCONT_1:20;
then f5|[.p,g.] is continuous by A17,A27,FCONT_1:18;
then
A29: f|[.p,g.] is continuous by A4,A28,FCONT_1:18;
A30: f4 is_differentiable_on Z by A7,A14,FDIFF_1:20;
then
A31: f5 is_differentiable_on Z by A19,A15,FDIFF_1:18;
[.p,g.] c= dom f by A28,VALUED_1:12;
then consider x0 such that
A32: x0 in ].p,g.[ and
A33: diff(f,x0)=0 by A1,A5,A29,A31,A26,A25,Th1,FDIFF_1:19;
take x0;
f is_differentiable_on Z by A5,A31,A26,FDIFF_1:19;
then diff(f,x0) = (f`|Z).x0 by A32,FDIFF_1:def 7
.= diff(f5,x0) - diff(f1,x0) by A5,A31,A26,A32,FDIFF_1:19
.= (f5`|Z).x0 - diff(f1,x0) by A31,A32,FDIFF_1:def 7
.= diff(f3,x0) + diff(f4,x0) - diff(f1,x0) by A19,A30,A15,A32,
FDIFF_1:18
.= (f3`|Z).x0 + diff(f4,x0) - diff(f1,x0) by A19,A32,FDIFF_1:def 7
.= 0 + diff(f4,x0) - diff(f1,x0) by A18,A12,A32,FDIFF_1:22
.= (f4`|Z).x0 - diff(f1,x0) by A30,A32,FDIFF_1:def 7
.= s*diff(f2,x0) - diff(f1,x0) by A7,A14,A32,FDIFF_1:20;
then
(diff(f2,x0)*(f1.g-f1.p))/(f2.g-f2.p)*(f2.g-f2.p) = diff(f1,x0)*(f2
.g-f2.p) by A33,XCMPLX_1:15;
hence x0 in ].p,g.[ & (f1.g-f1.p)*diff(f2,x0) = (f2.g-f2.p)*diff(f1,x0)
by A11,A32,XCMPLX_1:87;
end;
end;
hence thesis;
end;
::$N Cauchy Theorem
theorem
for x,t st 0<t for f1,f2 st [.x,x+t.] c= dom f1 & [.x,x+t.] c= dom f2
& f1|[.x,x+t.] is continuous & f1 is_differentiable_on ].x,x+t.[ & f2|[.x,x+t.]
is continuous & 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)
proof
let x,t such that
A1: 0<t;
let f1,f2 such that
A2: [.x,x+t.] c= dom f1 and
A3: [.x,x+t.] c= dom f2 and
A4: f1|[.x,x+t.] is continuous & f1 is_differentiable_on ].x,x+t.[ and
A5: f2|[.x,x+t.] is continuous & f2 is_differentiable_on ].x,x+t.[ and
A6: for x1 st x1 in ].x,x+t.[ holds diff(f2,x1)<>0;
consider x0 such that
A7: x0 in ].x,x+t.[ and
A8: (f1.(x+t)-f1.x)*diff(f2,x0)=(f2.(x+t)-f2.x)*diff(f1,x0) by A1,A2,A3,A4,A5
,Th5,XREAL_1:29;
diff(f2,x0)*((f1.(x+t)-f1.x)/diff(f2, x0))= (f2.(x+t)-f2.x)*diff(f1,x0)
/diff(f2,x0) by A8,XCMPLX_1:74;
then
(f1.(x+t)-f1.x)/(f2.(x+t)-f2.x) = (f2.(x+t)-f2.x)* (diff(f1,x0)/diff(f2
,x0))/(f2.(x+t)-f2.x) by A6,A7,XCMPLX_1:87;
then
A9: (f1.(x+t)-f1.x)/(f2.(x+t)-f2.x)=((diff(f1,x0)/diff(f2,x0))/(f2.(x+t) -
f2.x))* (f2.(x+t)-f2.x);
take s = (x0-x)/t;
x0 in {r: x<r & r<x+t} by A7,RCOMP_1:def 2;
then
A10: ex g st g=x0 & x<g & g<x+t;
then 0<x0-x by XREAL_1:50;
then 0/t < (x0-x)/t by A1,XREAL_1:74;
hence 0<s;
x0-x<t by A10,XREAL_1:19;
then (x0-x)/t<t/t by A1,XREAL_1:74;
hence s<1 by A1,XCMPLX_1:60;
A11: s*t+x = (x0-x)+x by A1,XCMPLX_1:87;
0<>f2.(x+t)-f2.x by A1,A3,A5,A6,Th1,XREAL_1:29;
hence thesis by A9,A11,XCMPLX_1:87;
end;
theorem Th7:
for p,g for f st ].p,g.[ c= dom f & f is_differentiable_on ].p,g
.[ & (for x st x in ].p,g.[ holds diff(f,x) = 0) holds f|].p,g.[ is constant
proof
let p,g;
let f such that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x st x in ].p,g.[ holds diff(f,x) = 0;
now
let x1,x2 be Element of REAL;
assume x1 in ].p,g.[ /\ dom f & x2 in ].p,g.[ /\ dom f;
then
A4: x1 in ].p,g.[ & x2 in ].p,g.[ by XBOOLE_0:def 4;
now
per cases;
suppose
x1=x2;
hence f.x1=f.x2;
end;
suppose
A5: not x1=x2;
now
per cases by A5,XXREAL_0:1;
suppose
A6: x1<x2;
then 0<>x2-x1;
then
A7: 0<>(x2-x1)" by XCMPLX_1:202;
reconsider Z=].x1,x2.[ as open Subset of REAL;
A8: [.x1,x2.] c= ].p,g.[ by A4,XXREAL_2:def 12;
f|].p,g.[ is continuous by A2,FDIFF_1:25;
then
A9: f|[.x1,x2.] is continuous by A8,FCONT_1:16;
A10: Z c= [.x1,x2.] by XXREAL_1:25;
then f is_differentiable_on Z by A2,A8,FDIFF_1:26,XBOOLE_1:1;
then
A11: ex x0 st x0 in ].x1,x2.[ & diff(f,x0) = (f.x2-f.x1)/(x2- x1)
by A1,A6,A8,A9,Th3,XBOOLE_1:1;
Z c= ].p,g.[ by A8,A10;
then 0 = (f.x2-f.x1) by A3,A7,A11,XCMPLX_1:6;
hence f.x1=f.x2;
end;
suppose
A12: x2<x1;
then 0<>x1-x2;
then
A13: 0<>(x1-x2)" by XCMPLX_1:202;
reconsider Z=].x2,x1.[ as open Subset of REAL;
A14: [.x2,x1.] c= ].p,g.[ by A4,XXREAL_2:def 12;
f|].p,g.[ is continuous by A2,FDIFF_1:25;
then
A15: f|[.x2,x1.] is continuous by A14,FCONT_1:16;
A16: Z c= [.x2,x1.] by XXREAL_1:25;
then f is_differentiable_on Z by A2,A14,FDIFF_1:26,XBOOLE_1:1;
then
A17: ex x0 st x0 in ].x2,x1.[ & diff(f,x0) = (f.x1-f.x2)/(x1- x2)
by A1,A12,A14,A15,Th3,XBOOLE_1:1;
Z c= ].p,g.[ by A14,A16;
then 0 = (f.x1-f.x2) by A3,A13,A17,XCMPLX_1:6;
hence f.x1=f.x2;
end;
end;
hence f.x1=f.x2;
end;
end;
hence f.x1=f.x2;
end;
hence thesis by PARTFUN2:58;
end;
theorem
for 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)|].p,g.[ is constant & ex r st for x st x in ].p,g.[ holds
f1.x = f2.x+r
proof
let p,g;
let f1,f2 such that
A1: f1 is_differentiable_on ].p,g.[ & f2 is_differentiable_on ].p,g.[ and
A2: for x st x in ].p,g.[ holds diff(f1,x) = diff(f2,x);
reconsider Z=].p,g.[ as open Subset of REAL;
].p,g.[ c= dom f1 & ].p,g.[ c= dom f2 by A1,FDIFF_1:def 6;
then ].p,g.[ c= dom f1 /\ dom f2 by XBOOLE_1:19;
then
A3: ].p,g.[ c= dom (f1-f2) by VALUED_1:12;
then
A4: f1-f2 is_differentiable_on Z by A1,FDIFF_1:19;
now
let x;
assume
A5: x in ].p,g.[;
hence diff(f1-f2,x) = ((f1-f2)`|Z).x by A4,FDIFF_1:def 7
.= diff(f1,x)-diff(f2,x) by A1,A3,A5,FDIFF_1:19
.= diff(f1,x)-diff(f1,x) by A2,A5
.= 0;
end;
hence (f1-f2)|].p,g.[ is constant by A1,A3,Th7,FDIFF_1:19;
then consider r being Element of REAL such that
A6: for x being Element of REAL
st x in ].p,g.[ /\ dom(f1-f2) holds (f1-f2).x = r
by PARTFUN2:57;
take r;
let x;
assume
A7: x in ].p,g.[;
then x in ].p,g.[ /\ dom(f1-f2) by A3,XBOOLE_1:28;
then r = (f1-f2).x by A6
.= f1.x - f2.x by A3,A7,VALUED_1:13;
hence thesis;
end;
theorem
for p,g for f st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & (
for x st x in ].p,g.[ holds 0<diff(f,x)) holds f|].p,g.[ is increasing
proof
let p,g;
let f such that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x st x in ].p,g.[ holds 0<diff(f,x);
now
let x1,x2 such that
A4: x1 in ].p,g.[ /\ dom f & x2 in ].p,g.[ /\ dom f and
A5: x1<x2;
A6: 0<x2-x1 by A5,XREAL_1:50;
reconsider Z=].x1,x2.[ as open Subset of REAL;
x1 in ].p,g.[ & x2 in ].p,g.[ by A4,XBOOLE_0:def 4;
then
A7: [.x1,x2.] c= ].p,g.[ by XXREAL_2:def 12;
f|].p,g.[ is continuous by A2,FDIFF_1:25;
then
A8: f|[.x1,x2.] is continuous by A7,FCONT_1:16;
A9: Z c= [.x1,x2.] by XXREAL_1:25;
then f is_differentiable_on Z by A2,A7,FDIFF_1:26,XBOOLE_1:1;
then
A10: ex x0 st x0 in ].x1,x2.[ & diff(f,x0) = (f.x2-f.x1)/(x2- x1) by A1,A5,A7
,A8,Th3,XBOOLE_1:1;
Z c= ].p,g.[ by A7,A9;
then 0<f.x2-f.x1 by A3,A6,A10;
then f.x1+0<f.x2 by XREAL_1:20;
hence f.x1<f.x2;
end;
hence thesis by RFUNCT_2:20;
end;
theorem
for p,g for f st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & (
for x st x in ].p,g.[ holds diff(f,x)<0) holds f|].p,g.[ is decreasing
proof
let p,g;
let f such that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x st x in ].p,g.[ holds diff(f,x)<0;
now
let x1,x2 such that
A4: x1 in ].p,g.[ /\ dom f & x2 in ].p,g.[ /\ dom f and
A5: x1<x2;
A6: 0<x2-x1 by A5,XREAL_1:50;
reconsider Z=].x1,x2.[ as open Subset of REAL;
x1 in ].p,g.[ & x2 in ].p,g.[ by A4,XBOOLE_0:def 4;
then
A7: [.x1,x2.] c= ].p,g.[ by XXREAL_2:def 12;
f|].p,g.[ is continuous by A2,FDIFF_1:25;
then
A8: f|[.x1,x2.] is continuous by A7,FCONT_1:16;
A9: Z c= [.x1,x2.] by XXREAL_1:25;
then f is_differentiable_on Z by A2,A7,FDIFF_1:26,XBOOLE_1:1;
then
A10: ex x0 st x0 in ].x1,x2.[ & diff(f,x0) = (f.x2-f.x1)/(x2- x1) by A1,A5,A7
,A8,Th3,XBOOLE_1:1;
Z c= ].p,g.[ by A7,A9;
then f.x2-f.x1<0 by A3,A6,A10;
then f.x2<f.x1+0 by XREAL_1:19;
hence f.x2<f.x1;
end;
hence thesis by RFUNCT_2:21;
end;
theorem
for p,g for f st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & (
for x st x in ].p,g.[ holds 0<=diff(f,x)) holds f|].p,g.[ is non-decreasing
proof
let p,g;
let f such that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x st x in ].p,g.[ holds 0<=diff(f,x);
now
let x1,x2 such that
A4: x1 in ].p,g.[ /\ dom f & x2 in ].p,g.[ /\ dom f and
A5: x1<x2;
A6: 0<>x2-x1 by A5;
reconsider Z=].x1,x2.[ as open Subset of REAL;
x1 in ].p,g.[ & x2 in ].p,g.[ by A4,XBOOLE_0:def 4;
then
A7: [.x1,x2.] c= ].p,g.[ by XXREAL_2:def 12;
f|].p,g.[ is continuous by A2,FDIFF_1:25;
then
A8: f|[.x1,x2.] is continuous by A7,FCONT_1:16;
A9: Z c= [.x1,x2.] by XXREAL_1:25;
then
A10: Z c= ].p,g.[ by A7;
f is_differentiable_on Z by A2,A7,A9,FDIFF_1:26,XBOOLE_1:1;
then
ex x0 st x0 in ].x1,x2.[ & diff(f,x0) = (f.x2-f.x1)/(x2- x1) by A1,A5,A7,A8
,Th3,XBOOLE_1:1;
then
A11: 0<=(f.x2-f.x1)/(x2-x1) by A3,A10;
0<=x2-x1 by A5,XREAL_1:50;
then 0*(x2-x1)<=(f.x2-f.x1)/(x2-x1)*(x2-x1) by A11;
then 0<=f.x2-f.x1 by A6,XCMPLX_1:87;
then f.x1+0<=f.x2 by XREAL_1:19;
hence f.x1<=f.x2;
end;
hence thesis by RFUNCT_2:22;
end;
theorem
for p,g for f st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & (
for x st x in ].p,g.[ holds diff(f,x)<=0) holds f|].p,g.[ is non-increasing
proof
let p,g;
let f such that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x st x in ].p,g.[ holds diff(f,x)<=0;
now
let x1,x2 such that
A4: x1 in ].p,g.[ /\ dom f & x2 in ].p,g.[ /\ dom f and
A5: x1<x2;
A6: 0<=x2-x1 by A5,XREAL_1:50;
reconsider Z=].x1,x2.[ as open Subset of REAL;
x1 in ].p,g.[ & x2 in ].p,g.[ by A4,XBOOLE_0:def 4;
then
A7: [.x1,x2.] c= ].p,g.[ by XXREAL_2:def 12;
f|].p,g.[ is continuous by A2,FDIFF_1:25;
then
A8: f|[.x1,x2.] is continuous by A7,FCONT_1:16;
A9: Z c= [.x1,x2.] by XXREAL_1:25;
then f is_differentiable_on Z by A2,A7,FDIFF_1:26,XBOOLE_1:1;
then
A10: ex x0 st x0 in ].x1,x2.[ & diff(f,x0) = (f.x2-f.x1)/(x2- x1) by A1,A5,A7
,A8,Th3,XBOOLE_1:1;
A11: 0<>x2-x1 by A5;
Z c= ].p,g.[ by A7,A9;
then (f.x2-f.x1)/(x2-x1)*(x2-x1)<=0*(x2-x1) by A3,A6,A10,XREAL_1:64;
then f.x2-f.x1<=0 by A11,XCMPLX_1:87;
then f.x2<=f.x1+0 by XREAL_1:20;
hence f.x2<=f.x1;
end;
hence thesis by RFUNCT_2:23;
end;