let p, g be Real; for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f,x) = 0 ) holds
f | ].p,g.[ is V8()
let f be PartFunc of REAL,REAL; ( ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f,x) = 0 ) implies f | ].p,g.[ is V8() )
assume that
A1:
].p,g.[ c= dom f
and
A2:
f is_differentiable_on ].p,g.[
and
A3:
for x being Real st x in ].p,g.[ holds
diff (f,x) = 0
; f | ].p,g.[ is V8()
now for x1, x2 being Element of REAL st x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) holds
f . x1 = f . x2let x1,
x2 be
Element of
REAL ;
( x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) implies f . x1 = f . x2 )assume
(
x1 in ].p,g.[ /\ (dom f) &
x2 in ].p,g.[ /\ (dom f) )
;
f . x1 = f . x2then A4:
(
x1 in ].p,g.[ &
x2 in ].p,g.[ )
by XBOOLE_0:def 4;
now f . x1 = f . x2per cases
( x1 = x2 or not x1 = x2 )
;
suppose A5:
not
x1 = x2
;
f . x1 = f . x2now f . x1 = f . x2per cases
( x1 < x2 or x2 < x1 )
by A5, XXREAL_0:1;
suppose A6:
x1 < x2
;
f . x1 = f . x2then
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 being
Real 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
;
verum end; suppose A12:
x2 < x1
;
f . x1 = f . x2then
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 being
Real 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
;
verum end; end; end; hence
f . x1 = f . x2
;
verum end; end; end; hence
f . x1 = f . x2
;
verum end;
hence
f | ].p,g.[ is V8()
by PARTFUN2:58; verum