let Z be open Subset of REAL; ( Z c= dom (ln * sec) implies ( ln * sec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * sec) `| Z) . x = (sin . x) / (cos . x) ) ) )
assume A1:
Z c= dom (ln * sec)
; ( ln * sec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * sec) `| Z) . x = (sin . x) / (cos . x) ) )
A2:
for x being Real st x in Z holds
sec . x > 0
dom (ln * sec) c= dom sec
by RELAT_1:25;
then A3:
Z c= dom sec
by A1, XBOOLE_1:1;
A4:
for x being Real st x in Z holds
cos . x <> 0
A5:
for x being Real st x in Z holds
sec is_differentiable_in x
A6:
for x being Real st x in Z holds
ln * sec is_differentiable_in x
then A7:
ln * sec is_differentiable_on Z
by A1, FDIFF_1:9;
for x being Real st x in Z holds
((ln * sec) `| Z) . x = (sin . x) / (cos . x)
proof
let x be
Real;
( x in Z implies ((ln * sec) `| Z) . x = (sin . x) / (cos . x) )
assume A8:
x in Z
;
((ln * sec) `| Z) . x = (sin . x) / (cos . x)
then A9:
cos . x <> 0
by A4;
(
sec is_differentiable_in x &
sec . x > 0 )
by A2, A5, A8;
then diff (
(ln * sec),
x) =
(diff (sec,x)) / (sec . x)
by TAYLOR_1:20
.=
((sin . x) / ((cos . x) ^2)) / (sec . x)
by A9, Th1
.=
((sin . x) / ((cos . x) ^2)) / ((cos . x) ")
by A3, A8, RFUNCT_1:def 2
.=
((sin . x) * (cos . x)) / ((cos . x) * (cos . x))
.=
(sin . x) / (cos . x)
by A4, A8, XCMPLX_1:91
;
hence
((ln * sec) `| Z) . x = (sin . x) / (cos . x)
by A7, A8, FDIFF_1:def 7;
verum
end;
hence
( ln * sec is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * sec) `| Z) . x = (sin . x) / (cos . x) ) )
by A1, A6, FDIFF_1:9; verum