let Z be open Subset of REAL ; :: thesis: ( Z c= dom ((id Z) (#) (cos * ((id Z) ^ ))) & not 0 in Z implies ( (id Z) (#) (cos * ((id Z) ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (cos * ((id Z) ^ ))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) ) ) )
set f = id Z;
assume A1:
( Z c= dom ((id Z) (#) (cos * ((id Z) ^ ))) & not 0 in Z )
; :: thesis: ( (id Z) (#) (cos * ((id Z) ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (cos * ((id Z) ^ ))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) ) )
then
Z c= (dom (id Z)) /\ (dom (cos * ((id Z) ^ )))
by VALUED_1:def 4;
then A2:
( Z c= dom (id Z) & Z c= dom (cos * ((id Z) ^ )) )
by XBOOLE_1:18;
A3:
for x being Real st x in Z holds
(id Z) . x = x
by FUNCT_1:35;
for y being set st y in Z holds
y in dom ((id Z) ^ )
by A2, FUNCT_1:21;
then A4:
Z c= dom ((id Z) ^ )
by TARSKI:def 3;
A5:
( cos * ((id Z) ^ ) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * ((id Z) ^ )) `| Z) . x = (1 / (x ^2 )) * (sin . (1 / x)) ) )
by A2, Th6, A1;
A6:
for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0
by FUNCT_1:35;
then A7:
( id Z is_differentiable_on Z & ( for x being Real st x in Z holds
((id Z) `| Z) . x = 1 ) )
by A2, FDIFF_1:31;
now let x be
Real;
:: thesis: ( x in Z implies (((id Z) (#) (cos * ((id Z) ^ ))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) )assume A8:
x in Z
;
:: thesis: (((id Z) (#) (cos * ((id Z) ^ ))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x)))A9:
x <> 0
by A8, A1;
(((id Z) (#) (cos * ((id Z) ^ ))) `| Z) . x =
(((cos * ((id Z) ^ )) . x) * (diff (id Z),x)) + (((id Z) . x) * (diff (cos * ((id Z) ^ )),x))
by A1, A5, A7, A8, FDIFF_1:29
.=
(((cos * ((id Z) ^ )) . x) * (((id Z) `| Z) . x)) + (((id Z) . x) * (diff (cos * ((id Z) ^ )),x))
by A7, A8, FDIFF_1:def 8
.=
(((cos * ((id Z) ^ )) . x) * 1) + (((id Z) . x) * (diff (cos * ((id Z) ^ )),x))
by A2, A6, A8, FDIFF_1:31
.=
((cos * ((id Z) ^ )) . x) + (x * (diff (cos * ((id Z) ^ )),x))
by A8, FUNCT_1:35
.=
((cos * ((id Z) ^ )) . x) + (x * (((cos * ((id Z) ^ )) `| Z) . x))
by A5, A8, FDIFF_1:def 8
.=
((cos * ((id Z) ^ )) . x) + (x * ((1 / (x ^2 )) * (sin . (1 / x))))
by A2, A8, Th6, A1
.=
((cos * ((id Z) ^ )) . x) + ((x * (1 / (x * x))) * (sin . (1 / x)))
.=
((cos * ((id Z) ^ )) . x) + ((x * ((1 / x) * (1 / x))) * (sin . (1 / x)))
by XCMPLX_1:103
.=
((cos * ((id Z) ^ )) . x) + (((x * (1 / x)) * (1 / x)) * (sin . (1 / x)))
.=
((cos * ((id Z) ^ )) . x) + ((1 * (1 / x)) * (sin . (1 / x)))
by A9, XCMPLX_1:107
.=
(cos . (((id Z) ^ ) . x)) + ((1 / x) * (sin . (1 / x)))
by A2, A8, FUNCT_1:22
.=
(cos . (((id Z) . x) " )) + ((1 / x) * (sin . (1 / x)))
by A4, A8, RFUNCT_1:def 8
.=
(cos . (1 * (x " ))) + ((1 / x) * (sin . (1 / x)))
by A3, A8
.=
(cos . (1 / x)) + ((1 / x) * (sin . (1 / x)))
by XCMPLX_0:def 9
;
hence
(((id Z) (#) (cos * ((id Z) ^ ))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x)))
;
:: thesis: verum end;
hence
( (id Z) (#) (cos * ((id Z) ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (cos * ((id Z) ^ ))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) ) )
by A1, A5, A7, FDIFF_1:29; :: thesis: verum