let x be Real; for n being Element of NAT
for Z being open Subset of REAL st x in Z holds
((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))
let n be Element of NAT ; for Z being open Subset of REAL st x in Z holds
((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))
let Z be open Subset of REAL; ( x in Z implies ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) )
assume A1:
x in Z
; ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))
dom (((- 1) (#) cos) | Z) =
(dom ((- 1) (#) cos)) /\ Z
by RELAT_1:61
.=
(dom cos) /\ Z
by VALUED_1:def 5
.=
Z
by SIN_COS:24, XBOOLE_1:28
;
then A2:
Z c= dom ((- 1) (#) cos)
by RELAT_1:60;
dom (((- 1) (#) sin) | Z) =
(dom ((- 1) (#) sin)) /\ Z
by RELAT_1:61
.=
(dom sin) /\ Z
by VALUED_1:def 5
.=
Z
by SIN_COS:24, XBOOLE_1:28
;
then A3:
Z c= dom ((- 1) (#) sin)
by RELAT_1:60;
A4:
sin is_differentiable_on Z
by FDIFF_1:26, SIN_COS:68;
then A5:
(- 1) (#) sin is_differentiable_on Z
by FDIFF_2:19;
A6:
cos is_differentiable_on Z
by FDIFF_1:26, SIN_COS:67;
then A7:
(- 1) (#) cos is_differentiable_on Z
by FDIFF_2:19;
per cases
( n > 0 or n = 0 )
;
suppose
n > 0
;
((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))then
0 < 0 + n
;
then
1
<= n
by NAT_1:19;
then reconsider i =
n - 1 as
Element of
NAT by INT_1:5;
now ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))per cases
( i is even or i is odd )
;
suppose
i is
even
;
((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))then consider j being
Nat such that A8:
i = 2
* j
by ABIAN:def 2;
per cases
( j is even or j is odd )
;
suppose
j is
even
;
((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))then consider m being
Nat such that A9:
j = 2
* m
by ABIAN:def 2;
((diff (sin,Z)) . (i + 1)) . x =
(((diff (sin,Z)) . (2 * j)) `| Z) . x
by A8, TAYLOR_1:def 5
.=
((((- 1) |^ j) (#) (sin | Z)) `| Z) . x
by TAYLOR_2:19
.=
(((1 |^ (2 * m)) (#) (sin | Z)) `| Z) . x
by A9, WSIERP_1:2
.=
((1 (#) (sin | Z)) `| Z) . x
.=
((sin | Z) `| Z) . x
by RFUNCT_1:21
.=
(sin `| Z) . x
by A4, FDIFF_2:16
.=
diff (
sin,
x)
by A1, A4, FDIFF_1:def 7
.=
cos . x
by SIN_COS:64
.=
cos . (x + ((2 * PI) * m))
by SIN_COS2:11
.=
sin . ((x + ((i / 2) * PI)) + (PI / 2))
by A8, A9, SIN_COS:78
.=
sin . (x + ((n * PI) / 2))
;
hence
((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))
;
verum end; suppose
j is
odd
;
((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))then consider s being
Nat such that A10:
j = (2 * s) + 1
by ABIAN:9;
((diff (sin,Z)) . (i + 1)) . x =
(((diff (sin,Z)) . (2 * j)) `| Z) . x
by A8, TAYLOR_1:def 5
.=
((((- 1) |^ ((2 * s) + 1)) (#) (sin | Z)) `| Z) . x
by A10, TAYLOR_2:19
.=
(((((- 1) |^ (2 * s)) * (- 1)) (#) (sin | Z)) `| Z) . x
by NEWTON:6
.=
((((1 |^ (2 * s)) * (- 1)) (#) (sin | Z)) `| Z) . x
by WSIERP_1:2
.=
(((1 * (- 1)) (#) (sin | Z)) `| Z) . x
.=
(((- sin) | Z) `| Z) . x
by RFUNCT_1:49
.=
(((- 1) (#) sin) `| Z) . x
by A5, FDIFF_2:16
.=
(- 1) * (diff (sin,x))
by A1, A3, A4, FDIFF_1:20
.=
(- 1) * (cos . x)
by SIN_COS:64
.=
- (cos . x)
.=
cos . (x + PI)
by SIN_COS:78
.=
cos . ((x + PI) + ((2 * PI) * s))
by SIN_COS2:11
.=
sin . ((x + ((i / 2) * PI)) + (PI / 2))
by A8, A10, SIN_COS:78
.=
sin . (x + ((n * PI) / 2))
;
hence
((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))
;
verum end; end; end; suppose
i is
odd
;
((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))then consider j being
Nat such that A11:
i = (2 * j) + 1
by ABIAN:9;
per cases
( j is even or j is odd )
;
suppose
j is
even
;
((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))then consider m being
Nat such that A12:
j = 2
* m
by ABIAN:def 2;
((diff (sin,Z)) . (i + 1)) . x =
(((diff (sin,Z)) . ((2 * j) + 1)) `| Z) . x
by A11, TAYLOR_1:def 5
.=
((((- 1) |^ (2 * m)) (#) (cos | Z)) `| Z) . x
by A12, TAYLOR_2:19
.=
(((1 |^ (2 * m)) (#) (cos | Z)) `| Z) . x
by WSIERP_1:2
.=
((1 (#) (cos | Z)) `| Z) . x
.=
((cos | Z) `| Z) . x
by RFUNCT_1:21
.=
(cos `| Z) . x
by A6, FDIFF_2:16
.=
diff (
cos,
x)
by A1, A6, FDIFF_1:def 7
.=
- (sin . x)
by SIN_COS:63
.=
sin . (x + PI)
by SIN_COS:78
.=
sin . ((x + PI) + ((2 * PI) * m))
by SIN_COS2:10
.=
sin . ((x + (((i - 1) / 2) * PI)) + PI)
by A11, A12
.=
sin . (x + ((n * PI) / 2))
;
hence
((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))
;
verum end; suppose
j is
odd
;
((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))then consider s being
Nat such that A13:
j = (2 * s) + 1
by ABIAN:9;
((diff (sin,Z)) . (i + 1)) . x =
(((diff (sin,Z)) . ((2 * j) + 1)) `| Z) . x
by A11, TAYLOR_1:def 5
.=
((((- 1) |^ j) (#) (cos | Z)) `| Z) . x
by TAYLOR_2:19
.=
(((((- 1) |^ (2 * s)) * (- 1)) (#) (cos | Z)) `| Z) . x
by A13, NEWTON:6
.=
((((1 |^ (2 * s)) * (- 1)) (#) (cos | Z)) `| Z) . x
by WSIERP_1:2
.=
(((1 * (- 1)) (#) (cos | Z)) `| Z) . x
.=
(((- cos) | Z) `| Z) . x
by RFUNCT_1:49
.=
(((- 1) (#) cos) `| Z) . x
by A7, FDIFF_2:16
.=
(- 1) * (diff (cos,x))
by A1, A2, A6, FDIFF_1:20
.=
(- 1) * (- (sin . x))
by SIN_COS:63
.=
sin . (x + ((2 * PI) * s))
by SIN_COS2:10
.=
sin . ((x + (((i - 3) / 2) * PI)) + (2 * PI))
by A11, A13, SIN_COS:78
.=
sin . (x + ((n * PI) / 2))
;
hence
((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))
;
verum end; end; end; end; end; hence
((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))
;
verum end; end;