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