let Z be open Subset of REAL; :: thesis: ( 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 ; :: thesis: ( 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

ln * ln is_differentiable_in x

for x being Real st x in Z holds

((ln * ln) `| Z) . x = 1 / ((ln . x) * x)

((ln * ln) `| Z) . x = 1 / ((ln . x) * x) ) ) by A1, A5, FDIFF_1:9; :: thesis: verum

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

proof

A5:
for x being Real st x in Z holds
let x be Real; :: thesis: ( x in Z implies ln . x > 0 )

assume x in Z ; :: thesis: ln . x > 0

then A4: ln . x in right_open_halfline 0 by A1, FUNCT_1:11, TAYLOR_1:18;

].0,+infty.[ = { g where g is Real : 0 < g } by XXREAL_1:230;

then ex g being Real st

( ln . x = g & 0 < g ) by A4;

hence ln . x > 0 ; :: thesis: verum

end;assume x in Z ; :: thesis: ln . x > 0

then A4: ln . x in right_open_halfline 0 by A1, FUNCT_1:11, TAYLOR_1:18;

].0,+infty.[ = { g where g is Real : 0 < g } by XXREAL_1:230;

then ex g being Real st

( ln . x = g & 0 < g ) by A4;

hence ln . x > 0 ; :: thesis: verum

ln * ln is_differentiable_in x

proof

then A8:
ln * ln is_differentiable_on Z
by A1, FDIFF_1:9;
let x be Real; :: thesis: ( x in Z implies ln * ln is_differentiable_in x )

assume A6: x in Z ; :: thesis: ln * ln is_differentiable_in x

then A7: ln . x > 0 by A3;

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

hence ln * ln is_differentiable_in x by A7, TAYLOR_1:20; :: thesis: verum

end;assume A6: x in Z ; :: thesis: ln * ln is_differentiable_in x

then A7: ln . x > 0 by A3;

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

hence ln * ln is_differentiable_in x by A7, TAYLOR_1:20; :: thesis: verum

for x being Real st x in Z holds

((ln * ln) `| Z) . x = 1 / ((ln . x) * x)

proof

hence
( ln * ln is_differentiable_on Z & ( for x being Real st x in Z holds
let x be Real; :: thesis: ( 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 ; :: thesis: ((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; :: thesis: verum

end;A9: ].0,+infty.[ = { g where g is Real : 0 < g } by XXREAL_1:230;

assume A10: x in Z ; :: thesis: ((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; :: thesis: verum

((ln * ln) `| Z) . x = 1 / ((ln . x) * x) ) ) by A1, A5, FDIFF_1:9; :: thesis: verum