let n be Element of NAT ; :: thesis: for Z being open Subset of REAL
for f being PartFunc of REAL ,REAL st Z c= dom ((sin * f) (#) ((#Z n) * sin )) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (sin * f) (#) ((#Z n) * sin ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * sin )) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) )
let Z be open Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL st Z c= dom ((sin * f) (#) ((#Z n) * sin )) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (sin * f) (#) ((#Z n) * sin ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * sin )) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( Z c= dom ((sin * f) (#) ((#Z n) * sin )) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) implies ( (sin * f) (#) ((#Z n) * sin ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * sin )) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) ) )
assume A1:
( Z c= dom ((sin * f) (#) ((#Z n) * sin )) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) )
; :: thesis: ( (sin * f) (#) ((#Z n) * sin ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * sin )) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) )
then
Z c= (dom (sin * f)) /\ (dom ((#Z n) * sin ))
by VALUED_1:def 4;
then A2:
( Z c= dom (sin * f) & Z c= dom ((#Z n) * sin ) )
by XBOOLE_1:18;
then
for y being set st y in Z holds
y in dom f
by FUNCT_1:21;
then A3:
Z c= dom f
by TARSKI:def 3;
A4:
for x being Real st x in Z holds
f . x = (n * x) + 0
by A1;
then A5:
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = n ) )
by A3, FDIFF_1:31;
for x being Real st x in Z holds
sin * f is_differentiable_in x
then A7:
sin * f is_differentiable_on Z
by A2, FDIFF_1:16;
A8:
for x being Real st x in Z holds
((sin * f) `| Z) . x = n * (cos . (n * x))
proof
let x be
Real;
:: thesis: ( x in Z implies ((sin * f) `| Z) . x = n * (cos . (n * x)) )
assume A9:
x in Z
;
:: thesis: ((sin * f) `| Z) . x = n * (cos . (n * x))
then A10:
f is_differentiable_in x
by A5, FDIFF_1:16;
sin is_differentiable_in f . x
by SIN_COS:69;
then diff (sin * f),
x =
(diff sin ,(f . x)) * (diff f,x)
by A10, FDIFF_2:13
.=
(cos . (f . x)) * (diff f,x)
by SIN_COS:69
.=
(cos . (n * x)) * (diff f,x)
by A1, A9
.=
(cos . (n * x)) * ((f `| Z) . x)
by A5, A9, FDIFF_1:def 8
.=
n * (cos . (n * x))
by A3, A4, A9, FDIFF_1:31
;
hence
((sin * f) `| Z) . x = n * (cos . (n * x))
by A7, A9, FDIFF_1:def 8;
:: thesis: verum
end;
then A11:
(#Z n) * sin is_differentiable_on Z
by A2, FDIFF_1:16;
A12:
for x being Real st x in Z holds
(((#Z n) * sin ) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . x)
now let x be
Real;
:: thesis: ( x in Z implies (((sin * f) (#) ((#Z n) * sin )) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) )assume A14:
x in Z
;
:: thesis: (((sin * f) (#) ((#Z n) * sin )) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x))A15:
n - 1 is
Element of
NAT
by A1, NAT_1:21;
(((sin * f) (#) ((#Z n) * sin )) `| Z) . x =
((((#Z n) * sin ) . x) * (diff (sin * f),x)) + (((sin * f) . x) * (diff ((#Z n) * sin ),x))
by A1, A7, A11, A14, FDIFF_1:29
.=
(((#Z n) . (sin . x)) * (diff (sin * f),x)) + (((sin * f) . x) * (diff ((#Z n) * sin ),x))
by A2, A14, FUNCT_1:22
.=
(((sin . x) #Z n) * (diff (sin * f),x)) + (((sin * f) . x) * (diff ((#Z n) * sin ),x))
by TAYLOR_1:def 1
.=
(((sin . x) #Z n) * (((sin * f) `| Z) . x)) + (((sin * f) . x) * (diff ((#Z n) * sin ),x))
by A7, A14, FDIFF_1:def 8
.=
(((sin . x) #Z n) * (n * (cos . (n * x)))) + (((sin * f) . x) * (diff ((#Z n) * sin ),x))
by A8, A14
.=
(((sin . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (f . x)) * (diff ((#Z n) * sin ),x))
by A2, A14, FUNCT_1:22
.=
(((sin . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (n * x)) * (diff ((#Z n) * sin ),x))
by A1, A14
.=
(((sin . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (n * x)) * ((((#Z n) * sin ) `| Z) . x))
by A11, A14, FDIFF_1:def 8
.=
(((sin . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (n * x)) * ((n * ((sin . x) #Z (n - 1))) * (cos . x)))
by A12, A14
.=
(((sin . x) #Z ((n - 1) + 1)) * (n * (cos . (n * x)))) + ((((sin . (n * x)) * n) * ((sin . x) #Z (n - 1))) * (cos . x))
.=
((((sin . x) #Z (n - 1)) * ((sin . x) #Z 1)) * (n * (cos . (n * x)))) + ((((sin . (n * x)) * n) * ((sin . x) #Z (n - 1))) * (cos . x))
by A15, TAYLOR_1:1
.=
((((sin . x) #Z (n - 1)) * (sin . x)) * (n * (cos . (n * x)))) + ((((sin . (n * x)) * n) * ((sin . x) #Z (n - 1))) * (cos . x))
by PREPOWER:45
.=
(n * ((sin . x) #Z (n - 1))) * (((sin . x) * (cos . (n * x))) + ((cos . x) * (sin . (n * x))))
.=
(n * ((sin . x) #Z (n - 1))) * (sin . (x + (n * x)))
by SIN_COS:79
.=
(n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x))
;
hence
(((sin * f) (#) ((#Z n) * sin )) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x))
;
:: thesis: verum end;
hence
( (sin * f) (#) ((#Z n) * sin ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * sin )) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) )
by A1, A7, A11, FDIFF_1:29; :: thesis: verum