let Z be open Subset of REAL; ( Z c= dom (sin * ln) & ( for x being Real st x in Z holds
x > 0 ) implies ( sin * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * ln) `| Z) . x = (cos . (ln . x)) / x ) ) )
assume that
A1:
Z c= dom (sin * ln)
and
A2:
for x being Real st x in Z holds
x > 0
; ( sin * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * ln) `| Z) . x = (cos . (ln . x)) / x ) )
A3:
for x being Real st x in Z holds
sin * ln is_differentiable_in x
then A5:
sin * ln is_differentiable_on Z
by A1, FDIFF_1:9;
for x being Real st x in Z holds
((sin * ln) `| Z) . x = (cos . (ln . x)) / x
proof
let x be
Real;
( x in Z implies ((sin * ln) `| Z) . x = (cos . (ln . x)) / x )
A6:
sin is_differentiable_in ln . x
by SIN_COS:64;
assume A7:
x in Z
;
((sin * ln) `| Z) . x = (cos . (ln . x)) / x
then
x > 0
by A2;
then A8:
x in right_open_halfline 0
by Lm3;
ln is_differentiable_in x
by A2, A7, TAYLOR_1:18;
then diff (
(sin * ln),
x) =
(diff (sin,(ln . x))) * (diff (ln,x))
by A6, FDIFF_2:13
.=
(cos . (ln . x)) * (diff (ln,x))
by SIN_COS:64
.=
(cos . (ln . x)) * (1 / x)
by A8, TAYLOR_1:18
.=
(cos . (ln . x)) / x
by XCMPLX_1:99
;
hence
((sin * ln) `| Z) . x = (cos . (ln . x)) / x
by A5, A7, FDIFF_1:def 7;
verum
end;
hence
( sin * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * ln) `| Z) . x = (cos . (ln . x)) / x ) )
by A1, A3, FDIFF_1:9; verum