let f be PartFunc of REAL ,REAL ; :: thesis: ( [#] 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 Z:
[#] REAL c= dom f
; :: thesis: ( not f is_differentiable_on [#] REAL or ex x0 being Real st not diff f,x0 <= 0 or f | ([#] REAL ) is non-increasing )
assume A1:
( f is_differentiable_on [#] REAL & ( for x0 being Real holds diff f,x0 <= 0 ) )
; :: thesis: f | ([#] REAL ) is non-increasing
now let r1,
r2 be
Real;
:: thesis: ( r1 in ([#] REAL ) /\ (dom f) & r2 in ([#] REAL ) /\ (dom f) & r1 < r2 implies f . r2 <= f . r1 )assume A2:
(
r1 in ([#] REAL ) /\ (dom f) &
r2 in ([#] REAL ) /\ (dom f) &
r1 < r2 )
;
:: thesis: f . r2 <= f . r1then A3:
(
r1 in dom f &
r2 in dom f &
r1 < r2 )
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 A4:
(
(min r1,r2) - 1
< r1 - 0 &
(min r1,r2) - 1
< r2 - 0 )
by XREAL_1:17;
A5:
(
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 A4;
then A6:
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 A4, A5;
then A7:
r2 in ].((min r1,r2) - 1),((max r1,r2) + 1).[
by RCOMP_1:def 2;
A8:
(min r1,r2) - 1
< (max r1,r2) + 1
by A4, A5, XXREAL_0:2;
A9:
f is_differentiable_on ].((min r1,r2) - 1),((max r1,r2) + 1).[
by A1, FDIFF_1:34;
X10:
].((min r1,r2) - 1),((max r1,r2) + 1).[ c= dom f
by Z, XBOOLE_1:1;
for
g1 being
Real st
g1 in ].((min r1,r2) - 1),((max r1,r2) + 1).[ holds
diff f,
g1 <= 0
by A1;
then A10:
f | ].((min r1,r2) - 1),((max r1,r2) + 1).[ is
non-increasing
by A8, A9, X10, ROLLE:12;
A11:
r1 in ].((min r1,r2) - 1),((max r1,r2) + 1).[ /\ (dom f)
by A3, A6, XBOOLE_0:def 4;
r2 in ].((min r1,r2) - 1),((max r1,r2) + 1).[ /\ (dom f)
by A3, A7, XBOOLE_0:def 4;
hence
f . r2 <= f . r1
by A2, A10, A11, RFUNCT_2:46;
:: thesis: verum end;
hence
f | ([#] REAL ) is non-increasing
by RFUNCT_2:46; :: thesis: verum