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) = ].0,+infty.[ by TAYLOR_1:def 4;
then G1: dom ((#R x) | (right_open_halfline 0)) = right_open_halfline 0 by RELAT_1:62;
K2: AffineMap ((- x),(x - 1)) is_differentiable_on right_open_halfline 0 by FDIFF_1:26, LemmaAffine;
TR: ((#R x) | (right_open_halfline 0)) | (right_open_halfline 0) = (#R x) | (right_open_halfline 0) by RELAT_1:72;
(#R x) | (right_open_halfline 0) is_differentiable_on right_open_halfline 0
proof
for z being Real st z in right_open_halfline 0 holds
((#R x) | (right_open_halfline 0)) | (right_open_halfline 0) is_differentiable_in z
proof
let z be Real; :: thesis: ( z in right_open_halfline 0 implies ((#R x) | (right_open_halfline 0)) | (right_open_halfline 0) is_differentiable_in z )
assume W0: z in right_open_halfline 0 ; :: thesis: ((#R x) | (right_open_halfline 0)) | (right_open_halfline 0) is_differentiable_in z
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 FDIFF_1:def 4, TAYLOR_1:21;
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 RCOMP_1:18, W0;
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) | (right_open_halfline 0)) by FX, Wa, G1;
for x being Real st x in N1 holds
(((#R x) | (right_open_halfline 0)) . x) - (((#R x) | (right_open_halfline 0)) . z) = (L . (x - z)) + (R . (x - z))
proof
let x be Real; :: thesis: ( x in N1 implies (((#R x) | (right_open_halfline 0)) . x) - (((#R x) | (right_open_halfline 0)) . z) = (L . (x - z)) + (R . (x - z)) )
assume F1: x in N1 ; :: thesis: (((#R x) | (right_open_halfline 0)) . x) - (((#R x) | (right_open_halfline 0)) . z) = (L . (x - z)) + (R . (x - z))
then ( (#R x) . x = ((#R x) | (right_open_halfline 0)) . x & (#R x) . z = ((#R x) | (right_open_halfline 0)) . z ) by FUNCT_1:49, Wa, FX, W0;
hence (((#R x) | (right_open_halfline 0)) . x) - (((#R x) | (right_open_halfline 0)) . z) = (L . (x - z)) + (R . (x - z)) by F1, R2, FX; :: thesis: verum
end;
hence ((#R x) | (right_open_halfline 0)) | (right_open_halfline 0) is_differentiable_in z by TR, FDIFF_1:def 4, R4; :: thesis: verum
end;
hence (#R x) | (right_open_halfline 0) is_differentiable_on right_open_halfline 0 by G1, FDIFF_1:def 6; :: 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 FDIFF_1:26, XXREAL_1:247;
k2: AffineMap ((- x),(x - 1)) is_differentiable_on Y by FDIFF_1:26, LemmaAffine;
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 G0, XBOOLE_1:19;
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 K2, FDIFF_1:18, G2;
then ga: (#R x) + (AffineMap ((- x),(x - 1))) is_differentiable_on Y by FDIFF_1:26, XXREAL_1:247;
az: dom ((#R x) + (AffineMap ((- x),(x - 1)))) = (dom (#R x)) /\ (dom (AffineMap ((- x),(x - 1)))) by VALUED_1:def 1
.= (right_open_halfline 0) /\ (dom (AffineMap ((- x),(x - 1)))) by TAYLOR_1:def 4
.= (right_open_halfline 0) /\ 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 k2, g2, Sa, FDIFF_1:9;
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 TAYLOR_1:21, Sb;
then diff ((#R x),y) = x * (y to_power (x - 1)) by POWER:def 2, Sb;
then H3: diff (((#R x) + (AffineMap ((- x),(x - 1)))),y) = (x * (y to_power (x - 1))) - x by H1, LemmaAffine
.= x * ((y to_power (x - 1)) - 1) ;
x - 1 < 1 - 1 by ZZ, XREAL_1:9;
then y to_power (x - 1) > y to_power 0 by POWER:40, Sb;
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 XREAL_1:129, H3, ZZ; :: thesis: verum
end;
hence ((#R x) + (AffineMap ((- x),(x - 1)))) | ].0,1.[ is increasing by ROLLE:9, ga, az, XXREAL_1:247; :: thesis: verum