let p, g be Real; ( p < g implies for f being PartFunc of REAL,REAL st [.p,g.] c= dom f & f | [.p,g.] is continuous & f is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) ) )
assume A1:
p < g
; for f being PartFunc of REAL,REAL st [.p,g.] c= dom f & f | [.p,g.] is continuous & f is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) )
A2:
0 <> g - p
by A1;
reconsider Z = ].p,g.[ as open Subset of REAL ;
defpred S1[ set ] means $1 in [.p,g.];
let f be PartFunc of REAL,REAL; ( [.p,g.] c= dom f & f | [.p,g.] is continuous & f is_differentiable_on ].p,g.[ implies ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) ) )
assume that
A3:
[.p,g.] c= dom f
and
A4:
f | [.p,g.] is continuous
and
A5:
f is_differentiable_on ].p,g.[
; ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) )
set r = ((f . g) - (f . p)) / (g - p);
deffunc H1( Real) -> Element of REAL = In (((((f . g) - (f . p)) / (g - p)) * ($1 - p)),REAL);
consider f1 being PartFunc of REAL,REAL such that
A6:
( ( for x being Element of REAL holds
( x in dom f1 iff S1[x] ) ) & ( for x being Element of REAL st x in dom f1 holds
f1 . x = H1(x) ) )
from SEQ_1:sch 3();
A7:
for x being Real st x in dom f1 holds
f1 . x = (((f . g) - (f . p)) / (g - p)) * (x - p)
proof
let x be
Real;
( x in dom f1 implies f1 . x = (((f . g) - (f . p)) / (g - p)) * (x - p) )
assume A8:
x in dom f1
;
f1 . x = (((f . g) - (f . p)) / (g - p)) * (x - p)
reconsider x =
x as
Real ;
f1 . x = H1(
x)
by A6, A8;
hence
f1 . x = (((f . g) - (f . p)) / (g - p)) * (x - p)
;
verum
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 (f - f1)
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 (f - f1)
by VALUED_1:12;
then A16: (f - f1) . p =
(f . p) - (f1 . p)
by A13, VALUED_1:13
.=
(f . p) - ((((f . g) - (f . p)) / (g - p)) * (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 for x being Real st x in Z holds
f1 . x = ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p))let x be
Real;
( x in Z implies f1 . x = ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p)) )assume
x in Z
;
f1 . x = ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p))then
x in dom f1
by A17, A6;
hence f1 . x =
(((f . g) - (f . p)) / (g - p)) * (x - p)
by A7
.=
((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p))
;
verum end;
then A20:
f1 is_differentiable_on Z
by A18, FDIFF_1:23;
now for x being Real st x in [.p,g.] holds
f1 . x = ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p))let x be
Real;
( x in [.p,g.] implies f1 . x = ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p)) )assume
x in [.p,g.]
;
f1 . x = ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p))then
x in dom f1
by A6;
hence f1 . x =
(((f . g) - (f . p)) / (g - p)) * (x - p)
by A7
.=
((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p))
;
verum end;
then
f1 | [.p,g.] is continuous
by FCONT_1:41;
then A21:
(f - f1) | [.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 (f - f1)
by VALUED_1:12;
(f - f1) . 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
.=
(f - f1) . p
by A16
;
then consider x0 being Real such that
A25:
x0 in ].p,g.[
and
A26:
diff ((f - f1),x0) = 0
by A1, A5, A20, A11, A21, A24, Th1, FDIFF_1:19;
take
x0
; ( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) )
f - f1 is_differentiable_on Z
by A5, A20, A24, FDIFF_1:19;
then diff ((f - f1),x0) =
((f - f1) `| 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
( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) )
by A18, A19, A25, A26, FDIFF_1:23; verum