let Z be open Subset of REAL; ( Z c= dom (ln * ln) & ( for x being Real st x in Z holds
x > 0 ) implies ( ln * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ln) `| Z) . x = 1 / ((ln . x) * x) ) ) )
assume that
A1:
Z c= dom (ln * ln)
and
A2:
for x being Real st x in Z holds
x > 0
; ( ln * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ln) `| Z) . x = 1 / ((ln . x) * x) ) )
A3:
for x being Real st x in Z holds
ln . x > 0
A5:
for x being Real st x in Z holds
ln * ln is_differentiable_in x
then A8:
ln * ln is_differentiable_on Z
by A1, FDIFF_1:9;
for x being Real st x in Z holds
((ln * ln) `| Z) . x = 1 / ((ln . x) * x)
proof
let x be
Real;
( x in Z implies ((ln * ln) `| Z) . x = 1 / ((ln . x) * x) )
A9:
].0,+infty.[ = { g where g is Real : 0 < g }
by XXREAL_1:230;
assume A10:
x in Z
;
((ln * ln) `| Z) . x = 1 / ((ln . x) * x)
then A11:
ln . x > 0
by A3;
x > 0
by A2, A10;
then A12:
x in right_open_halfline 0
by A9;
ln is_differentiable_in x
by A2, A10, TAYLOR_1:18;
then diff (
(ln * ln),
x) =
(diff (ln,x)) / (ln . x)
by A11, TAYLOR_1:20
.=
(1 / (ln . x)) * (1 / x)
by A12, TAYLOR_1:18
.=
1
/ ((ln . x) * x)
by XCMPLX_1:102
;
hence
((ln * ln) `| Z) . x = 1
/ ((ln . x) * x)
by A8, A10, FDIFF_1:def 7;
verum
end;
hence
( ln * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ln) `| Z) . x = 1 / ((ln . x) * x) ) )
by A1, A5, FDIFF_1:9; verum