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
0 <= diff (f,x) ) holds
f | ].p,g.[ is non-decreasing
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
0 <= diff (f,x) ) implies f | ].p,g.[ is non-decreasing )
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
0 <= diff (f,x)
; f | ].p,g.[ is non-decreasing
now for x1, x2 being Real st x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) & x1 < x2 holds
f . x1 <= f . x2let x1,
x2 be
Real;
( x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) & x1 < x2 implies f . x1 <= f . x2 )assume that A4:
(
x1 in ].p,g.[ /\ (dom f) &
x2 in ].p,g.[ /\ (dom f) )
and A5:
x1 < x2
;
f . x1 <= f . x2A6:
0 <> x2 - x1
by A5;
reconsider Z =
].x1,x2.[ as
open Subset of
REAL ;
(
x1 in ].p,g.[ &
x2 in ].p,g.[ )
by A4, XBOOLE_0:def 4;
then A7:
[.x1,x2.] c= ].p,g.[
by XXREAL_2:def 12;
f | ].p,g.[ is
continuous
by A2, FDIFF_1:25;
then A8:
f | [.x1,x2.] is
continuous
by A7, FCONT_1:16;
A9:
Z c= [.x1,x2.]
by XXREAL_1:25;
then A10:
Z c= ].p,g.[
by A7;
f is_differentiable_on Z
by A2, A7, A9, FDIFF_1:26, XBOOLE_1:1;
then
ex
x0 being
Real st
(
x0 in ].x1,x2.[ &
diff (
f,
x0)
= ((f . x2) - (f . x1)) / (x2 - x1) )
by A1, A5, A7, A8, Th3, XBOOLE_1:1;
then A11:
0 <= ((f . x2) - (f . x1)) / (x2 - x1)
by A3, A10;
0 <= x2 - x1
by A5, XREAL_1:50;
then
0 * (x2 - x1) <= (((f . x2) - (f . x1)) / (x2 - x1)) * (x2 - x1)
by A11;
then
0 <= (f . x2) - (f . x1)
by A6, XCMPLX_1:87;
then
(f . x1) + 0 <= f . x2
by XREAL_1:19;
hence
f . x1 <= f . x2
;
verum end;
hence
f | ].p,g.[ is non-decreasing
by RFUNCT_2:22; verum