let n be Element of NAT ; for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) )
let Z be open Subset of REAL; for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) )
let f be PartFunc of REAL,REAL; ( Z c= dom ((sin * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) implies ( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) )
assume that
A1:
Z c= dom ((sin * f) (#) ((#Z n) * cos))
and
A2:
n >= 1
and
A3:
for x being Real st x in Z holds
f . x = n * x
; ( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) )
A4:
for x being Real st x in Z holds
f . x = (n * x) + 0
by A3;
A5:
Z c= (dom (sin * f)) /\ (dom ((#Z n) * cos))
by A1, VALUED_1:def 4;
then A6:
Z c= dom (sin * f)
by XBOOLE_1:18;
then
for y being object st y in Z holds
y in dom f
by FUNCT_1:11;
then A7:
Z c= dom f
;
then A8:
f is_differentiable_on Z
by A4, FDIFF_1:23;
for x being Real st x in Z holds
sin * f is_differentiable_in x
then A10:
sin * f is_differentiable_on Z
by A6, FDIFF_1:9;
A11:
for x being Real st x in Z holds
((sin * f) `| Z) . x = n * (cos . (n * x))
proof
let x be
Real;
( x in Z implies ((sin * f) `| Z) . x = n * (cos . (n * x)) )
A12:
sin is_differentiable_in f . x
by SIN_COS:64;
assume A13:
x in Z
;
((sin * f) `| Z) . x = n * (cos . (n * x))
then
f is_differentiable_in x
by A8, FDIFF_1:9;
then diff (
(sin * f),
x) =
(diff (sin,(f . x))) * (diff (f,x))
by A12, FDIFF_2:13
.=
(cos . (f . x)) * (diff (f,x))
by SIN_COS:64
.=
(cos . (n * x)) * (diff (f,x))
by A3, A13
.=
(cos . (n * x)) * ((f `| Z) . x)
by A8, A13, FDIFF_1:def 7
.=
n * (cos . (n * x))
by A7, A4, A13, FDIFF_1:23
;
hence
((sin * f) `| Z) . x = n * (cos . (n * x))
by A10, A13, FDIFF_1:def 7;
verum
end;
A14:
Z c= dom ((#Z n) * cos)
by A5, XBOOLE_1:18;
then A15:
(#Z n) * cos is_differentiable_on Z
by A14, FDIFF_1:9;
A16:
for x being Real st x in Z holds
(((#Z n) * cos) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . x))
now for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x))let x be
Real;
( x in Z implies (((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) )A18:
n - 1 is
Element of
NAT
by A2, NAT_1:21;
assume A19:
x in Z
;
(((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x))then (((sin * f) (#) ((#Z n) * cos)) `| Z) . x =
((((#Z n) * cos) . x) * (diff ((sin * f),x))) + (((sin * f) . x) * (diff (((#Z n) * cos),x)))
by A1, A10, A15, FDIFF_1:21
.=
(((#Z n) . (cos . x)) * (diff ((sin * f),x))) + (((sin * f) . x) * (diff (((#Z n) * cos),x)))
by A14, A19, FUNCT_1:12
.=
(((cos . x) #Z n) * (diff ((sin * f),x))) + (((sin * f) . x) * (diff (((#Z n) * cos),x)))
by TAYLOR_1:def 1
.=
(((cos . x) #Z n) * (((sin * f) `| Z) . x)) + (((sin * f) . x) * (diff (((#Z n) * cos),x)))
by A10, A19, FDIFF_1:def 7
.=
(((cos . x) #Z n) * (n * (cos . (n * x)))) + (((sin * f) . x) * (diff (((#Z n) * cos),x)))
by A11, A19
.=
(((cos . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (f . x)) * (diff (((#Z n) * cos),x)))
by A6, A19, FUNCT_1:12
.=
(((cos . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (n * x)) * (diff (((#Z n) * cos),x)))
by A3, A19
.=
(((cos . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (n * x)) * ((((#Z n) * cos) `| Z) . x))
by A15, A19, FDIFF_1:def 7
.=
(((cos . x) #Z ((n - 1) + 1)) * (n * (cos . (n * x)))) + ((sin . (n * x)) * (- ((n * ((cos . x) #Z (n - 1))) * (sin . x))))
by A16, A19
.=
((((cos . x) #Z (n - 1)) * ((cos . x) #Z 1)) * (n * (cos . (n * x)))) + ((sin . (n * x)) * (- ((n * ((cos . x) #Z (n - 1))) * (sin . x))))
by A18, TAYLOR_1:1
.=
((((cos . x) #Z (n - 1)) * ((cos . x) #Z 1)) * (n * (cos . (n * x)))) - ((((sin . (n * x)) * n) * ((cos . x) #Z (n - 1))) * (sin . x))
.=
((((cos . x) #Z (n - 1)) * (cos . x)) * (n * (cos . (n * x)))) - ((((sin . (n * x)) * n) * ((cos . x) #Z (n - 1))) * (sin . x))
by PREPOWER:35
.=
(n * ((cos . x) #Z (n - 1))) * (((cos . (n * x)) * (cos . x)) - ((sin . x) * (sin . (n * x))))
.=
(n * ((cos . x) #Z (n - 1))) * (cos . (x + (n * x)))
by SIN_COS:74
.=
(n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x))
;
hence
(((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x))
;
verum end;
hence
( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) )
by A1, A10, A15, FDIFF_1:21; verum