let f be PartFunc of REAL ,REAL ; :: thesis: ( f is total & ( for r1, r2 being Real holds abs ((f . r1) - (f . r2)) <= (r1 - r2) ^2 ) implies ( f is_differentiable_on [#] REAL & f | ([#] REAL ) is constant ) )
assume A1:
( f is total & ( for r1, r2 being Real holds abs ((f . r1) - (f . r2)) <= (r1 - r2) ^2 ) )
; :: thesis: ( f is_differentiable_on [#] REAL & f | ([#] REAL ) is constant )
then A2:
dom f = [#] REAL
by PARTFUN1:def 4;
A3:
for r1, r2 being Real st r1 in [#] REAL & r2 in [#] REAL holds
abs ((f . r1) - (f . r2)) <= (r1 - r2) ^2
by A1;
now let r1,
r2 be
Real;
:: thesis: ( r1 in ([#] REAL ) /\ (dom f) & r2 in ([#] REAL ) /\ (dom f) implies f . r1 = f . r2 )assume
(
r1 in ([#] REAL ) /\ (dom f) &
r2 in ([#] REAL ) /\ (dom f) )
;
:: thesis: f . r1 = f . r2then A4:
(
r1 in dom f &
r2 in dom f )
by XBOOLE_0:def 4;
set rn =
min r1,
r2;
set rx =
max r1,
r2;
(
min r1,
r2 <= r1 &
min r1,
r2 <= r2 )
by XXREAL_0:17;
then A5:
(
(min r1,r2) - 1
< r1 - 0 &
(min r1,r2) - 1
< r2 - 0 )
by XREAL_1:17;
A6:
(
r1 + 0 < (max r1,r2) + 1 &
r2 + 0 < (max r1,r2) + 1 )
by XREAL_1:10, XXREAL_0:25;
then
r1 in { g1 where g1 is Real : ( (min r1,r2) - 1 < g1 & g1 < (max r1,r2) + 1 ) }
by A5;
then A7:
r1 in ].((min r1,r2) - 1),((max r1,r2) + 1).[
by RCOMP_1:def 2;
r2 in { g2 where g2 is Real : ( (min r1,r2) - 1 < g2 & g2 < (max r1,r2) + 1 ) }
by A5, A6;
then A8:
r2 in ].((min r1,r2) - 1),((max r1,r2) + 1).[
by RCOMP_1:def 2;
A9:
(min r1,r2) - 1
< (max r1,r2) + 1
by A5, A6, XXREAL_0:2;
for
g1,
g2 being
Real st
g1 in ].((min r1,r2) - 1),((max r1,r2) + 1).[ &
g2 in ].((min r1,r2) - 1),((max r1,r2) + 1).[ holds
abs ((f . g1) - (f . g2)) <= (g1 - g2) ^2
by A1;
then A10:
f | ].((min r1,r2) - 1),((max r1,r2) + 1).[ is
constant
by A2, A9, Th25;
A11:
r1 in ].((min r1,r2) - 1),((max r1,r2) + 1).[ /\ (dom f)
by A4, A7, XBOOLE_0:def 4;
r2 in ].((min r1,r2) - 1),((max r1,r2) + 1).[ /\ (dom f)
by A4, A8, XBOOLE_0:def 4;
hence
f . r1 = f . r2
by A10, A11, PARTFUN2:77;
:: thesis: verum end;
hence
( f is_differentiable_on [#] REAL & f | ([#] REAL ) is constant )
by A2, A3, Th24, PARTFUN2:77; :: thesis: verum