let f be PartFunc of REAL,REAL; ( [#] REAL c= dom f & f is_differentiable_on [#] REAL & ( for x0 being Real holds diff (f,x0) <= 0 ) implies f | ([#] REAL) is non-increasing )
assume A1:
[#] REAL c= dom f
; ( not f is_differentiable_on [#] REAL or ex x0 being Real st not diff (f,x0) <= 0 or f | ([#] REAL) is non-increasing )
assume that
A2:
f is_differentiable_on [#] REAL
and
A3:
for x0 being Real holds diff (f,x0) <= 0
; f | ([#] REAL) is non-increasing
now let r1,
r2 be
Real;
( r1 in ([#] REAL) /\ (dom f) & r2 in ([#] REAL) /\ (dom f) & r1 < r2 implies f . r2 <= f . r1 )assume that A4:
r1 in ([#] REAL) /\ (dom f)
and A5:
r2 in ([#] REAL) /\ (dom f)
and A6:
r1 < r2
;
f . r2 <= f . r1set rx =
max (
r1,
r2);
set rn =
min (
r1,
r2);
A7:
r2 + 0 < (max (r1,r2)) + 1
by XREAL_1:8, XXREAL_0:25;
(min (r1,r2)) - 1
< r2 - 0
by XREAL_1:15, XXREAL_0:17;
then
r2 in { g2 where g2 is Real : ( (min (r1,r2)) - 1 < g2 & g2 < (max (r1,r2)) + 1 ) }
by A7;
then A8:
r2 in ].((min (r1,r2)) - 1),((max (r1,r2)) + 1).[
by RCOMP_1:def 2;
r2 in dom f
by A5, XBOOLE_0:def 4;
then A9:
r2 in ].((min (r1,r2)) - 1),((max (r1,r2)) + 1).[ /\ (dom f)
by A8, XBOOLE_0:def 4;
A10:
for
g1 being
Real st
g1 in ].((min (r1,r2)) - 1),((max (r1,r2)) + 1).[ holds
diff (
f,
g1)
<= 0
by A3;
f is_differentiable_on ].((min (r1,r2)) - 1),((max (r1,r2)) + 1).[
by A2, FDIFF_1:26;
then A11:
f | ].((min (r1,r2)) - 1),((max (r1,r2)) + 1).[ is
non-increasing
by A1, A10, ROLLE:12, XBOOLE_1:1;
A12:
r1 + 0 < (max (r1,r2)) + 1
by XREAL_1:8, XXREAL_0:25;
(min (r1,r2)) - 1
< r1 - 0
by XREAL_1:15, XXREAL_0:17;
then
r1 in { g1 where g1 is Real : ( (min (r1,r2)) - 1 < g1 & g1 < (max (r1,r2)) + 1 ) }
by A12;
then A13:
r1 in ].((min (r1,r2)) - 1),((max (r1,r2)) + 1).[
by RCOMP_1:def 2;
r1 in dom f
by A4, XBOOLE_0:def 4;
then
r1 in ].((min (r1,r2)) - 1),((max (r1,r2)) + 1).[ /\ (dom f)
by A13, XBOOLE_0:def 4;
hence
f . r2 <= f . r1
by A6, A11, A9, RFUNCT_2:23;
verum end;
hence
f | ([#] REAL) is non-increasing
by RFUNCT_2:23; verum