let Z be open Subset of REAL; ( Z c= dom (cosec * ln) implies ( cosec * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * ln) `| Z) . x = - ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2))) ) ) )
assume A1:
Z c= dom (cosec * ln)
; ( cosec * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * ln) `| Z) . x = - ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2))) ) )
dom (cosec * ln) c= dom ln
by RELAT_1:25;
then A2:
Z c= dom ln
by A1, XBOOLE_1:1;
A3:
for x being Real st x in Z holds
x > 0
A4:
for x being Real st x in Z holds
diff (ln,x) = 1 / x
A5:
for x being Real st x in Z holds
sin . (ln . x) <> 0
A6:
for x being Real st x in Z holds
cosec * ln is_differentiable_in x
then A9:
cosec * ln is_differentiable_on Z
by A1, FDIFF_1:9;
for x being Real st x in Z holds
((cosec * ln) `| Z) . x = - ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)))
proof
let x be
Real;
( x in Z implies ((cosec * ln) `| Z) . x = - ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2))) )
assume A10:
x in Z
;
((cosec * ln) `| Z) . x = - ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)))
then A11:
ln is_differentiable_in x
by A3, TAYLOR_1:18;
A12:
sin . (ln . x) <> 0
by A5, A10;
then
cosec is_differentiable_in ln . x
by Th2;
then diff (
(cosec * ln),
x) =
(diff (cosec,(ln . x))) * (diff (ln,x))
by A11, FDIFF_2:13
.=
(- ((cos . (ln . x)) / ((sin . (ln . x)) ^2))) * (diff (ln,x))
by A12, Th2
.=
(1 / x) * ((- (cos . (ln . x))) / ((sin . (ln . x)) ^2))
by A4, A10
.=
(1 * (- (cos . (ln . x)))) / (x * ((sin . (ln . x)) ^2))
by XCMPLX_1:76
;
hence
((cosec * ln) `| Z) . x = - ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)))
by A9, A10, FDIFF_1:def 7;
verum
end;
hence
( cosec * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * ln) `| Z) . x = - ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2))) ) )
by A1, A6, FDIFF_1:9; verum