let p, g be Real; :: thesis: ( p < g implies 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 increasing )
assume
p < g
; :: thesis: 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 increasing
let f be PartFunc of REAL ,REAL ; :: thesis: ( ].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 increasing )
assume that
A0:
].p,g.[ c= dom f
and
A1:
f is_differentiable_on ].p,g.[
and
A2:
for x being Real st x in ].p,g.[ holds
0 < diff f,x
; :: thesis: f | ].p,g.[ is increasing
now let x1,
x2 be
Real;
:: thesis: ( x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) & x1 < x2 implies f . x1 < f . x2 )assume that A3:
(
x1 in ].p,g.[ /\ (dom f) &
x2 in ].p,g.[ /\ (dom f) )
and A4:
x1 < x2
;
:: thesis: f . x1 < f . x2A5:
(
x1 in ].p,g.[ &
x2 in ].p,g.[ )
by A3, XBOOLE_0:def 4;
reconsider Z =
].x1,x2.[ as
open Subset of
REAL ;
A6:
[.x1,x2.] c= ].p,g.[
by A5, XXREAL_2:def 12;
A7:
Z c= [.x1,x2.]
by XXREAL_1:25;
then A8:
Z c= ].p,g.[
by A6, XBOOLE_1:1;
A9:
0 < x2 - x1
by A4, XREAL_1:52;
f | ].p,g.[ is
continuous
by A1, FDIFF_1:33;
then A11:
f | [.x1,x2.] is
continuous
by A6, FCONT_1:17;
f is_differentiable_on Z
by A1, A6, A7, FDIFF_1:34, XBOOLE_1:1;
then consider x0 being
Real such that A12:
(
x0 in ].x1,x2.[ &
diff f,
x0 = ((f . x2) - (f . x1)) / (x2 - x1) )
by A4, A11, Th3, A0, A6, XBOOLE_1:1;
0 < (f . x2) - (f . x1)
by A9, A2, A8, A12;
then
(f . x1) + 0 < f . x2
by XREAL_1:22;
hence
f . x1 < f . x2
;
:: thesis: verum end;
hence
f | ].p,g.[ is increasing
by RFUNCT_2:43; :: thesis: verum