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

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} = {}

((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 )

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) )

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

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

then A6:
right_open_halfline number_e c= right_open_halfline 0
;
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;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

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

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

((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

P3:
g is_differentiable_on right_open_halfline number_e
by FDIFF_1:26, A4, A6;
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;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

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

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

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

hence
(id ([#] REAL)) / (g | (right_open_halfline number_e)) is non-decreasing
by P1, P3, FDIFF_2:35; :: thesis: verum
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;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