let Z be open Subset of REAL; :: thesis: ( Z c= dom (- (cos * ln)) implies ( - (cos * ln) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cos * ln)) `| Z) . x = (sin . (log (number_e,x))) / x ) ) )

assume A1: Z c= dom (- (cos * ln)) ; :: thesis: ( - (cos * ln) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cos * ln)) `| Z) . x = (sin . (log (number_e,x))) / x ) )

then A2: Z c= dom (cos * ln) by VALUED_1:8;

then for y being object st y in Z holds

y in dom ln by FUNCT_1:11;

then A3: Z c= dom ln by TARSKI:def 3;

then A4: ln is_differentiable_on Z by FDIFF_1:26, TAYLOR_1:18;

for x being Real st x in Z holds

cos * ln is_differentiable_in x

A7: for x being Real st x in Z holds

((- (cos * ln)) `| Z) . x = (sin . (log (number_e,x))) / x

hence ( - (cos * ln) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cos * ln)) `| Z) . x = (sin . (log (number_e,x))) / x ) ) by A6, A7, FDIFF_1:20; :: thesis: verum

((- (cos * ln)) `| Z) . x = (sin . (log (number_e,x))) / x ) ) )

assume A1: Z c= dom (- (cos * ln)) ; :: thesis: ( - (cos * ln) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cos * ln)) `| Z) . x = (sin . (log (number_e,x))) / x ) )

then A2: Z c= dom (cos * ln) by VALUED_1:8;

then for y being object st y in Z holds

y in dom ln by FUNCT_1:11;

then A3: Z c= dom ln by TARSKI:def 3;

then A4: ln is_differentiable_on Z by FDIFF_1:26, TAYLOR_1:18;

for x being Real st x in Z holds

cos * ln is_differentiable_in x

proof

then A6:
cos * ln is_differentiable_on Z
by A2, FDIFF_1:9;
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 A5: ln is_differentiable_in x by A4, FDIFF_1:9;

cos is_differentiable_in ln . x by SIN_COS:63;

hence cos * ln is_differentiable_in x by A5, FDIFF_2:13; :: thesis: verum

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

then A5: ln is_differentiable_in x by A4, FDIFF_1:9;

cos is_differentiable_in ln . x by SIN_COS:63;

hence cos * ln is_differentiable_in x by A5, FDIFF_2:13; :: thesis: verum

A7: for x being Real st x in Z holds

((- (cos * ln)) `| Z) . x = (sin . (log (number_e,x))) / x

proof

Z c= dom ((- 1) (#) (cos * ln))
by A1;
let x be Real; :: thesis: ( x in Z implies ((- (cos * ln)) `| Z) . x = (sin . (log (number_e,x))) / x )

A8: cos is_differentiable_in ln . x by SIN_COS:63;

assume A9: x in Z ; :: thesis: ((- (cos * ln)) `| Z) . x = (sin . (log (number_e,x))) / x

then A10: x in right_open_halfline 0 by A2, FUNCT_1:11, TAYLOR_1:18;

A11: ln is_differentiable_in x by A4, A9, FDIFF_1:9;

((- (cos * ln)) `| Z) . x = (- 1) * (diff ((cos * ln),x)) by A1, A6, A9, FDIFF_1:20

.= (- 1) * ((diff (cos,(ln . x))) * (diff (ln,x))) by A11, A8, FDIFF_2:13

.= (- 1) * ((- (sin . (ln . x))) * (diff (ln,x))) by SIN_COS:63

.= ((- 1) * (- (sin . (ln . x)))) * (diff (ln,x))

.= ((- 1) * (- (sin . (log (number_e,x))))) * (diff (ln,x)) by A10, TAYLOR_1:def 2

.= ((- 1) * (- (sin . (log (number_e,x))))) * (1 / x) by A3, A9, TAYLOR_1:18

.= (sin . (log (number_e,x))) / x by XCMPLX_1:99 ;

hence ((- (cos * ln)) `| Z) . x = (sin . (log (number_e,x))) / x ; :: thesis: verum

end;A8: cos is_differentiable_in ln . x by SIN_COS:63;

assume A9: x in Z ; :: thesis: ((- (cos * ln)) `| Z) . x = (sin . (log (number_e,x))) / x

then A10: x in right_open_halfline 0 by A2, FUNCT_1:11, TAYLOR_1:18;

A11: ln is_differentiable_in x by A4, A9, FDIFF_1:9;

((- (cos * ln)) `| Z) . x = (- 1) * (diff ((cos * ln),x)) by A1, A6, A9, FDIFF_1:20

.= (- 1) * ((diff (cos,(ln . x))) * (diff (ln,x))) by A11, A8, FDIFF_2:13

.= (- 1) * ((- (sin . (ln . x))) * (diff (ln,x))) by SIN_COS:63

.= ((- 1) * (- (sin . (ln . x)))) * (diff (ln,x))

.= ((- 1) * (- (sin . (log (number_e,x))))) * (diff (ln,x)) by A10, TAYLOR_1:def 2

.= ((- 1) * (- (sin . (log (number_e,x))))) * (1 / x) by A3, A9, TAYLOR_1:18

.= (sin . (log (number_e,x))) / x by XCMPLX_1:99 ;

hence ((- (cos * ln)) `| Z) . x = (sin . (log (number_e,x))) / x ; :: thesis: verum

hence ( - (cos * ln) is_differentiable_on Z & ( for x being Real st x in Z holds

((- (cos * ln)) `| Z) . x = (sin . (log (number_e,x))) / x ) ) by A6, A7, FDIFF_1:20; :: thesis: verum