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