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

proof

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;

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