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