set g = (log (2,number_e)) (#) ln;
take
(log (2,number_e)) (#) ln
; ( 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
; ( ( 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)
( (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;
( d in right_open_halfline 0 implies ((log (2,number_e)) (#) ln) . d = log (2,d) )
assume A51:
d in right_open_halfline 0
;
((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
;
verum
end;
thus
(log (2,number_e)) (#) ln is_differentiable_on right_open_halfline 0
by FDIFF_1:20, A3, TAYLOR_1:18; 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) )
verumproof
let x be
Real;
( 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
;
( (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;
( 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
;
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;
verum
end;