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