let x, y be Element of [.0,1.]; :: thesis: ( 0 < x & x < 1 & 0 < y & y < 1 implies ((#R x) + (AffineMap ((- x),(x - 1)))) | ].0,1.[ is increasing )
assume ZZ: ( 0 < x & x < 1 & 0 < y & y < 1 ) ; :: thesis: ((#R x) + (AffineMap ((- x),(x - 1)))) | ].0,1.[ is increasing
set f1 = #R x;
set f2 = AffineMap ((- x),(x - 1));
reconsider Y = ].0,1.[ as open Subset of REAL ;
set f = (#R x) + (AffineMap ((- x),(x - 1)));
set A = right_open_halfline 0;
G0: right_open_halfline 0 c= dom (#R x) by TAYLOR_1:def 4;
dom (#R x) = by TAYLOR_1:def 4;
then G1: dom ((#R x) | ) = right_open_halfline 0 by RELAT_1:62;
K2: AffineMap ((- x),(x - 1)) is_differentiable_on right_open_halfline 0 by ;
TR: ((#R x) | ) | = (#R x) | by RELAT_1:72;
(#R x) | is_differentiable_on right_open_halfline 0
proof
for z being Real st z in right_open_halfline 0 holds
((#R x) | ) | is_differentiable_in z
proof
let z be Real; :: thesis: ( z in right_open_halfline 0 implies ((#R x) | ) | is_differentiable_in z )
assume W0: z in right_open_halfline 0 ; :: thesis:
then z > 0 by XXREAL_1:235;
then consider N being Neighbourhood of z such that
R1: ( N c= dom (#R x) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((#R x) . x) - ((#R x) . z) = (L . (x - z)) + (R . (x - z)) ) by ;
consider L being LinearFunc, R being RestFunc such that
R2: for x being Real st x in N holds
((#R x) . x) - ((#R x) . z) = (L . (x - z)) + (R . (x - z)) by R1;
set V = right_open_halfline 0;
consider V1 being Neighbourhood of z such that
Wa: V1 c= right_open_halfline 0 by ;
consider N1 being Neighbourhood of z such that
FX: ( N1 c= N & N1 c= V1 ) by RCOMP_1:17;
R4: N1 c= dom ((#R x) | ) by FX, Wa, G1;
for x being Real st x in N1 holds
(((#R x) | ) . x) - (((#R x) | ) . z) = (L . (x - z)) + (R . (x - z))
proof
let x be Real; :: thesis: ( x in N1 implies (((#R x) | ) . x) - (((#R x) | ) . z) = (L . (x - z)) + (R . (x - z)) )
assume F1: x in N1 ; :: thesis: (((#R x) | ) . x) - (((#R x) | ) . z) = (L . (x - z)) + (R . (x - z))
then ( (#R x) . x = ((#R x) | ) . x & (#R x) . z = ((#R x) | ) . z ) by ;
hence (((#R x) | ) . x) - (((#R x) | ) . z) = (L . (x - z)) + (R . (x - z)) by F1, R2, FX; :: thesis: verum
end;
hence ((#R x) | ) | is_differentiable_in z by ; :: thesis: verum
end;
hence (#R x) | is_differentiable_on right_open_halfline 0 by ; :: thesis: verum
end;
then G2: #R x is_differentiable_on right_open_halfline 0 by INTEGRA7:5;
then g2: #R x is_differentiable_on Y by ;
k2: AffineMap ((- x),(x - 1)) is_differentiable_on Y by ;
dom (AffineMap ((- x),(x - 1))) = REAL by FUNCT_2:def 1;
then right_open_halfline 0 c= (dom (#R x)) /\ (dom (AffineMap ((- x),(x - 1)))) by ;
then right_open_halfline 0 c= dom ((#R x) + (AffineMap ((- x),(x - 1)))) by VALUED_1:def 1;
then (#R x) + (AffineMap ((- x),(x - 1))) is_differentiable_on right_open_halfline 0 by ;
then ga: (#R x) + (AffineMap ((- x),(x - 1))) is_differentiable_on Y by ;
az: dom ((#R x) + (AffineMap ((- x),(x - 1)))) = (dom (#R x)) /\ (dom (AffineMap ((- x),(x - 1)))) by VALUED_1:def 1
.= /\ (dom (AffineMap ((- x),(x - 1)))) by TAYLOR_1:def 4
.= /\ REAL by FUNCT_2:def 1
.= right_open_halfline 0 by XBOOLE_1:28 ;
for y being Real st y in Y holds
0 < diff (((#R x) + (AffineMap ((- x),(x - 1)))),y)
proof
let y be Real; :: thesis: ( y in Y implies 0 < diff (((#R x) + (AffineMap ((- x),(x - 1)))),y) )
assume Sa: y in Y ; :: thesis: 0 < diff (((#R x) + (AffineMap ((- x),(x - 1)))),y)
then Sb: ( 0 < y & y < 1 ) by XXREAL_1:4;
( #R x is_differentiable_in y & AffineMap ((- x),(x - 1)) is_differentiable_in y ) by ;
then H1: diff (((#R x) + (AffineMap ((- x),(x - 1)))),y) = (diff ((#R x),y)) + (diff ((AffineMap ((- x),(x - 1))),y)) by FDIFF_1:13;
( #R x is_differentiable_in y & diff ((#R x),y) = x * (y #R (x - 1)) ) by ;
then diff ((#R x),y) = x * (y to_power (x - 1)) by ;
then H3: diff (((#R x) + (AffineMap ((- x),(x - 1)))),y) = (x * (y to_power (x - 1))) - x by
.= x * ((y to_power (x - 1)) - 1) ;
x - 1 < 1 - 1 by ;
then y to_power (x - 1) > y to_power 0 by ;
then y to_power (x - 1) > 1 by POWER:24;
then (y to_power (x - 1)) - 1 > 1 - 1 by XREAL_1:9;
hence 0 < diff (((#R x) + (AffineMap ((- x),(x - 1)))),y) by ; :: thesis: verum
end;
hence ((#R x) + (AffineMap ((- x),(x - 1)))) | ].0,1.[ is increasing by ; :: thesis: verum