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 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} <> {}
;
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;
verum
end;
take
(id ([#] REAL)) / (g | (right_open_halfline number_e))
; ( 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
; ( ( 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))
( (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;
( 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)))
;
((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))
;
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;
( 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
;
( (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;
verum
end;
hence P3:
(id ([#] REAL)) / (g | (right_open_halfline number_e)) is_differentiable_on right_open_halfline number_e
by P1; ( ( 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)
(id ([#] REAL)) / (g | (right_open_halfline number_e)) is non-decreasing proof
let x be
Real;
( 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
;
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;
verum
end;
hence
(id ([#] REAL)) / (g | (right_open_halfline number_e)) is non-decreasing
by P1, P3, FDIFF_2:35; verum