set g = (log (2,number_e)) (#) ln;

take (log (2,number_e)) (#) ln ; :: thesis: ( dom ((log (2,number_e)) (#) ln) = right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds

((log (2,number_e)) (#) ln) . x = log (2,x) ) & (log (2,number_e)) (#) ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds

( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) ) ) )

thus A3: dom ((log (2,number_e)) (#) ln) = dom ln by VALUED_1:def 5

.= right_open_halfline 0 by TAYLOR_1:def 2 ; :: thesis: ( ( for x being Real st x in right_open_halfline 0 holds

((log (2,number_e)) (#) ln) . x = log (2,x) ) & (log (2,number_e)) (#) ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds

( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) ) ) )

E1: number_e > 1 by XXREAL_0:2, TAYLOR_1:11;

thus for d being Real st d in right_open_halfline 0 holds

((log (2,number_e)) (#) ln) . d = log (2,d) :: thesis: ( (log (2,number_e)) (#) ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds

( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) ) ) )

( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) )

thus for x being Real st x in right_open_halfline 0 holds

( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) ) :: thesis: verum

take (log (2,number_e)) (#) ln ; :: thesis: ( dom ((log (2,number_e)) (#) ln) = right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds

((log (2,number_e)) (#) ln) . x = log (2,x) ) & (log (2,number_e)) (#) ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds

( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) ) ) )

thus A3: dom ((log (2,number_e)) (#) ln) = dom ln by VALUED_1:def 5

.= right_open_halfline 0 by TAYLOR_1:def 2 ; :: thesis: ( ( for x being Real st x in right_open_halfline 0 holds

((log (2,number_e)) (#) ln) . x = log (2,x) ) & (log (2,number_e)) (#) ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds

( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) ) ) )

E1: number_e > 1 by XXREAL_0:2, TAYLOR_1:11;

thus for d being Real st d in right_open_halfline 0 holds

((log (2,number_e)) (#) ln) . d = log (2,d) :: thesis: ( (log (2,number_e)) (#) ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds

( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) ) ) )

proof

thus
(log (2,number_e)) (#) ln is_differentiable_on right_open_halfline 0
by FDIFF_1:20, A3, TAYLOR_1:18; :: thesis: for x being Real st x in right_open_halfline 0 holds
let d be Real; :: thesis: ( d in right_open_halfline 0 implies ((log (2,number_e)) (#) ln) . d = log (2,d) )

assume A51: d in right_open_halfline 0 ; :: thesis: ((log (2,number_e)) (#) ln) . d = log (2,d)

then reconsider d0 = d as Element of right_open_halfline 0 ;

d in { y where y is Real : 0 < y } by XXREAL_1:230, A51;

then E3: ex y being Real st

( d = y & 0 < y ) ;

thus ((log (2,number_e)) (#) ln) . d = (log (2,number_e)) * (ln . d) by A3, A51, VALUED_1:def 5

.= (log (2,number_e)) * (log (number_e,d0)) by TAYLOR_1:def 2

.= log (2,d) by E1, E3, POWER:56 ; :: thesis: verum

end;assume A51: d in right_open_halfline 0 ; :: thesis: ((log (2,number_e)) (#) ln) . d = log (2,d)

then reconsider d0 = d as Element of right_open_halfline 0 ;

d in { y where y is Real : 0 < y } by XXREAL_1:230, A51;

then E3: ex y being Real st

( d = y & 0 < y ) ;

thus ((log (2,number_e)) (#) ln) . d = (log (2,number_e)) * (ln . d) by A3, A51, VALUED_1:def 5

.= (log (2,number_e)) * (log (number_e,d0)) by TAYLOR_1:def 2

.= log (2,d) by E1, E3, POWER:56 ; :: thesis: verum

( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) )

thus for x being Real st x in right_open_halfline 0 holds

( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) ) :: thesis: verum

proof

let x be Real; :: thesis: ( x in right_open_halfline 0 implies ( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) ) )

assume A1: x in right_open_halfline 0 ; :: thesis: ( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) )

A2: ln is_differentiable_in x by A1, TAYLOR_1:18;

hence (log (2,number_e)) (#) ln is_differentiable_in x by FDIFF_1:15; :: thesis: ( diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) )

A3: diff (ln,x) = 1 / x by A1, TAYLOR_1:18;

A4: diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) * (diff (ln,x)) by FDIFF_1:15, A2;

thus diff (((log (2,number_e)) (#) ln),x) = (1 * (log (2,number_e))) / x by XCMPLX_1:74, A4, A3

.= (log (2,number_e)) / x ; :: thesis: 0 < diff (((log (2,number_e)) (#) ln),x)

A5: 0 < diff (ln,x) by A1, TAYLOR_1:18;

log (2,2) < log (2,number_e) by POWER:57, TAYLOR_1:11;

then 0 < log (2,number_e) by POWER:52;

hence 0 < diff (((log (2,number_e)) (#) ln),x) by A4, A5; :: thesis: verum

end;assume A1: x in right_open_halfline 0 ; :: thesis: ( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) )

A2: ln is_differentiable_in x by A1, TAYLOR_1:18;

hence (log (2,number_e)) (#) ln is_differentiable_in x by FDIFF_1:15; :: thesis: ( diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) )

A3: diff (ln,x) = 1 / x by A1, TAYLOR_1:18;

A4: diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) * (diff (ln,x)) by FDIFF_1:15, A2;

thus diff (((log (2,number_e)) (#) ln),x) = (1 * (log (2,number_e))) / x by XCMPLX_1:74, A4, A3

.= (log (2,number_e)) / x ; :: thesis: 0 < diff (((log (2,number_e)) (#) ln),x)

A5: 0 < diff (ln,x) by A1, TAYLOR_1:18;

log (2,2) < log (2,number_e) by POWER:57, TAYLOR_1:11;

then 0 < log (2,number_e) by POWER:52;

hence 0 < diff (((log (2,number_e)) (#) ln),x) by A4, A5; :: thesis: verum