let x be Real; :: thesis: 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 ; :: thesis: 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; :: thesis: ( x in Z implies ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) )
assume A1: x in Z ; :: thesis: ((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 ; :: thesis: ((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 :: thesis: ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))
per cases ( i is even or i is odd ) ;
suppose i is even ; :: thesis: ((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 ; :: thesis: ((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)) ; :: thesis: verum
end;
suppose j is odd ; :: thesis: ((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)) ; :: thesis: verum
end;
end;
end;
suppose i is odd ; :: thesis: ((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 ; :: thesis: ((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)) ; :: thesis: verum
end;
suppose j is odd ; :: thesis: ((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)) ; :: thesis: verum
end;
end;
end;
end;
end;
hence ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) ; :: thesis: verum
end;
suppose A14: n = 0 ; :: thesis: ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))
then ((diff (sin,Z)) . n) . x = (sin | Z) . x by TAYLOR_1:def 5
.= sin . (x + ((n * PI) / 2)) by A1, A14, FUNCT_1:49 ;
hence ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) ; :: thesis: verum
end;
end;