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