let f be PartFunc of REAL,REAL; ( [#] REAL c= dom f & f is_differentiable_on [#] REAL & ( for x0 being Real holds 0 <= diff (f,x0) ) implies f | ([#] REAL) is non-decreasing )
assume
[#] REAL c= dom f
; ( not f is_differentiable_on [#] REAL or ex x0 being Real st not 0 <= diff (f,x0) or f | ([#] REAL) is non-decreasing )
assume that
A1:
f is_differentiable_on [#] REAL
and
A2:
for x0 being Real holds 0 <= diff (f,x0)
; f | ([#] REAL) is non-decreasing
now for r1, r2 being Real st r1 in ([#] REAL) /\ (dom f) & r2 in ([#] REAL) /\ (dom f) & r1 < r2 holds
f . r1 <= f . r2let r1,
r2 be
Real;
( r1 in ([#] REAL) /\ (dom f) & r2 in ([#] REAL) /\ (dom f) & r1 < r2 implies f . r1 <= f . r2 )assume that A3:
r1 in ([#] REAL) /\ (dom f)
and A4:
r2 in ([#] REAL) /\ (dom f)
and A5:
r1 < r2
;
f . r1 <= f . r2set rx =
max (
r1,
r2);
set rn =
min (
r1,
r2);
A6:
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 A6;
then A7:
r2 in ].((min (r1,r2)) - 1),((max (r1,r2)) + 1).[
by RCOMP_1:def 2;
r2 in dom f
by A4, XBOOLE_0:def 4;
then A8:
r2 in ].((min (r1,r2)) - 1),((max (r1,r2)) + 1).[ /\ (dom f)
by A7, XBOOLE_0:def 4;
A9:
for
g1 being
Real st
g1 in ].((min (r1,r2)) - 1),((max (r1,r2)) + 1).[ holds
0 <= diff (
f,
g1)
by A2;
f is_differentiable_on ].((min (r1,r2)) - 1),((max (r1,r2)) + 1).[
by A1, FDIFF_1:26;
then A10:
f | ].((min (r1,r2)) - 1),((max (r1,r2)) + 1).[ is
non-decreasing
by A9, ROLLE:11;
A11:
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 A11;
then A12:
r1 in ].((min (r1,r2)) - 1),((max (r1,r2)) + 1).[
by RCOMP_1:def 2;
r1 in dom f
by A3, XBOOLE_0:def 4;
then
r1 in ].((min (r1,r2)) - 1),((max (r1,r2)) + 1).[ /\ (dom f)
by A12, XBOOLE_0:def 4;
hence
f . r1 <= f . r2
by A5, A10, A8, RFUNCT_2:22;
verum end;
hence
f | ([#] REAL) is non-decreasing
by RFUNCT_2:22; verum