consider g being PartFunc of REAL,REAL such that
A2: dom g = right_open_halfline 0 and
A3: for x being Real st x in right_open_halfline 0 holds
g . x = log (2,x) and
A4: g is_differentiable_on right_open_halfline 0 and
A5: for x being Real st x in right_open_halfline 0 holds
( g is_differentiable_in x & diff (g,x) = (log (2,number_e)) / x & 0 < diff (g,x) ) by Lm6;
set g0 = g | (right_open_halfline number_e);
AA6: for x being object st x in right_open_halfline number_e holds
x in right_open_halfline 0
proof
let x be object ; :: thesis: ( x in right_open_halfline number_e implies x in right_open_halfline 0 )
assume x in right_open_halfline number_e ; :: thesis: x in right_open_halfline 0
then x in { y where y is Real : number_e < y } by XXREAL_1:230;
then consider y being Real such that
AA2: ( x = y & number_e < y ) ;
x in { z where z is Real : 0 < z } by TAYLOR_1:11, AA2;
hence x in right_open_halfline 0 by XXREAL_1:230; :: thesis: verum
end;
then A6: right_open_halfline number_e c= right_open_halfline 0 ;
then A7: dom (g | (right_open_halfline number_e)) = right_open_halfline number_e by RELAT_1:62, A2;
set f = (id ([#] REAL)) / (g | (right_open_halfline number_e));
G0: (g | (right_open_halfline number_e)) " {0} = {}
proof
assume (g | (right_open_halfline number_e)) " {0} <> {} ; :: thesis: contradiction
then consider x being object such that
P01: x in (g | (right_open_halfline number_e)) " {0} by XBOOLE_0:def 1;
P02: ( x in dom (g | (right_open_halfline number_e)) & (g | (right_open_halfline number_e)) . x in {0} ) by P01, FUNCT_1:def 7;
P04: (g | (right_open_halfline number_e)) . x = 0 by TARSKI:def 1, P02;
reconsider x0 = x as Real by P01;
x0 in { y where y is Real : number_e < y } by XXREAL_1:230, P02, A7;
then ex y being Real st
( x = y & number_e < y ) ;
then E5: 2 < x0 by XXREAL_0:2, TAYLOR_1:11;
F3: (g | (right_open_halfline number_e)) . x = g . x by FUNCT_1:49, P02, A7
.= log (2,x0) by A3, AA6, P02, A7 ;
log (2,2) <= log (2,x0) by E5, PRE_FF:10;
hence contradiction by POWER:52, P04, F3; :: thesis: verum
end;
take (id ([#] REAL)) / (g | (right_open_halfline number_e)) ; :: thesis: ( right_open_halfline number_e = dom ((id ([#] REAL)) / (g | (right_open_halfline number_e))) & ( for x being Real st x in dom ((id ([#] REAL)) / (g | (right_open_halfline number_e))) holds
((id ([#] REAL)) / (g | (right_open_halfline number_e))) . x = x / (log (2,x)) ) & (id ([#] REAL)) / (g | (right_open_halfline number_e)) is_differentiable_on right_open_halfline number_e & ( for x0 being Real st x0 in right_open_halfline number_e holds
0 <= diff (((id ([#] REAL)) / (g | (right_open_halfline number_e))),x0) ) & (id ([#] REAL)) / (g | (right_open_halfline number_e)) is non-decreasing )
thus P1: dom ((id ([#] REAL)) / (g | (right_open_halfline number_e))) = (dom (id ([#] REAL))) /\ ((dom (g | (right_open_halfline number_e))) \ ((g | (right_open_halfline number_e)) " {0})) by RFUNCT_1:def 1
.= right_open_halfline number_e by XBOOLE_1:28, A7, G0 ; :: thesis: ( ( for x being Real st x in dom ((id ([#] REAL)) / (g | (right_open_halfline number_e))) holds
((id ([#] REAL)) / (g | (right_open_halfline number_e))) . x = x / (log (2,x)) ) & (id ([#] REAL)) / (g | (right_open_halfline number_e)) is_differentiable_on right_open_halfline number_e & ( for x0 being Real st x0 in right_open_halfline number_e holds
0 <= diff (((id ([#] REAL)) / (g | (right_open_halfline number_e))),x0) ) & (id ([#] REAL)) / (g | (right_open_halfline number_e)) is non-decreasing )
thus for x being Real st x in dom ((id ([#] REAL)) / (g | (right_open_halfline number_e))) holds
((id ([#] REAL)) / (g | (right_open_halfline number_e))) . x = x / (log (2,x)) :: thesis: ( (id ([#] REAL)) / (g | (right_open_halfline number_e)) is_differentiable_on right_open_halfline number_e & ( for x0 being Real st x0 in right_open_halfline number_e holds
0 <= diff (((id ([#] REAL)) / (g | (right_open_halfline number_e))),x0) ) & (id ([#] REAL)) / (g | (right_open_halfline number_e)) is non-decreasing )
proof
let x be Real; :: thesis: ( x in dom ((id ([#] REAL)) / (g | (right_open_halfline number_e))) implies ((id ([#] REAL)) / (g | (right_open_halfline number_e))) . x = x / (log (2,x)) )
assume F1: x in dom ((id ([#] REAL)) / (g | (right_open_halfline number_e))) ; :: thesis: ((id ([#] REAL)) / (g | (right_open_halfline number_e))) . x = x / (log (2,x))
thus ((id ([#] REAL)) / (g | (right_open_halfline number_e))) . x = ((id ([#] REAL)) . x) * (((g | (right_open_halfline number_e)) . x) ") by F1, RFUNCT_1:def 1
.= x * (((g | (right_open_halfline number_e)) . x) ") by Lm5
.= x * ((g . x) ") by P1, F1, FUNCT_1:49
.= x * ((log (2,x)) ") by A3, P1, AA6, F1
.= x * (1 / (log (2,x))) by XCMPLX_1:215
.= (1 * x) / (log (2,x)) by XCMPLX_1:74
.= x / (log (2,x)) ; :: thesis: verum
end;
P3: g is_differentiable_on right_open_halfline number_e by FDIFF_1:26, A4, A6;
then XP: ( g | (right_open_halfline number_e) is_differentiable_on right_open_halfline number_e & g `| (right_open_halfline number_e) = (g | (right_open_halfline number_e)) `| (right_open_halfline number_e) ) by FDIFF_2:16;
F12: for x being Real st x in right_open_halfline number_e holds
( (id ([#] REAL)) / (g | (right_open_halfline number_e)) is_differentiable_in x & diff (((id ([#] REAL)) / (g | (right_open_halfline number_e))),x) = ((log (2,x)) - (log (2,number_e))) / ((log (2,x)) ^2) )
proof
let x be Real; :: thesis: ( x in right_open_halfline number_e implies ( (id ([#] REAL)) / (g | (right_open_halfline number_e)) is_differentiable_in x & diff (((id ([#] REAL)) / (g | (right_open_halfline number_e))),x) = ((log (2,x)) - (log (2,number_e))) / ((log (2,x)) ^2) ) )
assume F1: x in right_open_halfline number_e ; :: thesis: ( (id ([#] REAL)) / (g | (right_open_halfline number_e)) is_differentiable_in x & diff (((id ([#] REAL)) / (g | (right_open_halfline number_e))),x) = ((log (2,x)) - (log (2,number_e))) / ((log (2,x)) ^2) )
then FA: x in right_open_halfline 0 by AA6;
FB: diff (g,x) = (g `| (right_open_halfline number_e)) . x by P3, F1, FDIFF_1:def 7
.= diff ((g | (right_open_halfline number_e)),x) by XP, F1, FDIFF_1:def 7 ;
x in { y where y is Real : number_e < y } by XXREAL_1:230, F1;
then EE5: ex y being Real st
( x = y & number_e < y ) ;
then E5: 2 < x by XXREAL_0:2, TAYLOR_1:11;
F3: (g | (right_open_halfline number_e)) . x = g . x by F1, FUNCT_1:49
.= log (2,x) by F1, AA6, A3 ;
log (2,2) <= log (2,x) by E5, PRE_FF:10;
then F2: 0 < (g | (right_open_halfline number_e)) . x by F3, POWER:52;
F3: id ([#] REAL) is_differentiable_in x by Lm5;
F6: g | (right_open_halfline number_e) is_differentiable_in x by P3, F1;
diff (((id ([#] REAL)) / (g | (right_open_halfline number_e))),x) = (((diff ((id ([#] REAL)),x)) * ((g | (right_open_halfline number_e)) . x)) - ((diff ((g | (right_open_halfline number_e)),x)) * ((id ([#] REAL)) . x))) / (((g | (right_open_halfline number_e)) . x) ^2) by FDIFF_2:14, F2, F3, F6
.= ((1 * ((g | (right_open_halfline number_e)) . x)) - ((diff ((g | (right_open_halfline number_e)),x)) * ((id ([#] REAL)) . x))) / (((g | (right_open_halfline number_e)) . x) ^2) by Lm5
.= ((1 * ((g | (right_open_halfline number_e)) . x)) - ((diff ((g | (right_open_halfline number_e)),x)) * x)) / (((g | (right_open_halfline number_e)) . x) ^2) by Lm5
.= ((1 * (g . x)) - ((diff (g,x)) * x)) / (((g | (right_open_halfline number_e)) . x) ^2) by F1, FUNCT_1:49, FB
.= ((1 * (g . x)) - ((diff (g,x)) * x)) / ((g . x) ^2) by F1, FUNCT_1:49
.= ((1 * (log (2,x))) - ((diff (g,x)) * x)) / ((g . x) ^2) by A3, F1, AA6
.= ((1 * (log (2,x))) - ((diff (g,x)) * x)) / ((log (2,x)) ^2) by A3, AA6, F1
.= ((1 * (log (2,x))) - (((log (2,number_e)) / x) * x)) / ((log (2,x)) ^2) by A5, FA
.= ((log (2,x)) - (log (2,number_e))) / ((log (2,x)) ^2) by XCMPLX_1:87, EE5, TAYLOR_1:11 ;
hence ( (id ([#] REAL)) / (g | (right_open_halfline number_e)) is_differentiable_in x & diff (((id ([#] REAL)) / (g | (right_open_halfline number_e))),x) = ((log (2,x)) - (log (2,number_e))) / ((log (2,x)) ^2) ) by FDIFF_2:14, F2, F3, F6; :: thesis: verum
end;
hence P3: (id ([#] REAL)) / (g | (right_open_halfline number_e)) is_differentiable_on right_open_halfline number_e by P1; :: thesis: ( ( for x0 being Real st x0 in right_open_halfline number_e holds
0 <= diff (((id ([#] REAL)) / (g | (right_open_halfline number_e))),x0) ) & (id ([#] REAL)) / (g | (right_open_halfline number_e)) is non-decreasing )
thus for x being Real st x in right_open_halfline number_e holds
0 <= diff (((id ([#] REAL)) / (g | (right_open_halfline number_e))),x) :: thesis: (id ([#] REAL)) / (g | (right_open_halfline number_e)) is non-decreasing
proof
let x be Real; :: thesis: ( x in right_open_halfline number_e implies 0 <= diff (((id ([#] REAL)) / (g | (right_open_halfline number_e))),x) )
assume F1: x in right_open_halfline number_e ; :: thesis: 0 <= diff (((id ([#] REAL)) / (g | (right_open_halfline number_e))),x)
then P41: diff (((id ([#] REAL)) / (g | (right_open_halfline number_e))),x) = ((log (2,x)) - (log (2,number_e))) / ((log (2,x)) ^2) by F12;
x in { y where y is Real : number_e < y } by XXREAL_1:230, F1;
then ex y being Real st
( x = y & number_e < y ) ;
then log (2,number_e) < log (2,x) by POWER:57, TAYLOR_1:11;
then 0 < (log (2,x)) - (log (2,number_e)) by XREAL_1:50;
hence 0 <= diff (((id ([#] REAL)) / (g | (right_open_halfline number_e))),x) by P41; :: thesis: verum
end;
hence (id ([#] REAL)) / (g | (right_open_halfline number_e)) is non-decreasing by P1, P3, FDIFF_2:35; :: thesis: verum