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

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)

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

then G2:
#R x is_differentiable_on right_open_halfline 0
by INTEGRA7:5;
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

end;((#R x) | (right_open_halfline 0)) | (right_open_halfline 0) is_differentiable_in z

proof

hence
(#R x) | (right_open_halfline 0) is_differentiable_on right_open_halfline 0
by G1, FDIFF_1:def 6; :: thesis: verum
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))

end;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

hence
((#R x) | (right_open_halfline 0)) | (right_open_halfline 0) is_differentiable_in z
by TR, FDIFF_1:def 4, R4; :: thesis: verum
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;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

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

hence
((#R x) + (AffineMap ((- x),(x - 1)))) | ].0,1.[ is increasing
by ROLLE:9, ga, az, XXREAL_1:247; :: thesis: verum
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;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