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) (#) sin ) | Z) = (dom ((- 1) (#) sin )) /\ Z by RELAT_1:90
.= (dom sin ) /\ Z by VALUED_1:def 5
.= Z by SIN_COS:27, XBOOLE_1:28 ;
then A2: Z c= dom ((- 1) (#) sin ) by RELAT_1:89;
dom (((- 1) (#) cos ) | Z) = (dom ((- 1) (#) cos )) /\ Z by RELAT_1:90
.= (dom cos ) /\ Z by VALUED_1:def 5
.= Z by SIN_COS:27, XBOOLE_1:28 ;
then A3: Z c= dom ((- 1) (#) cos ) by RELAT_1:89;
A4: sin is_differentiable_on Z by FDIFF_1:34, SIN_COS:73;
then AA: (- 1) (#) sin is_differentiable_on Z by FDIFF_2:19;
A6: cos is_differentiable_on Z by FDIFF_1:34, SIN_COS:72;
then AAA: (- 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:18;

now

per cases ( i is even or not i is even ) ;

suppose i is even ; :: thesis: ((diff sin ,Z) . n) . x = sin . (x + ((n * PI ) / 2))

then consider j being Element of NAT such that
A8: i = 2 * j by ABIAN:def 2;

per cases ( j is even or not j is even ) ;

suppose j is even ; :: thesis: ((diff sin ,Z) . n) . x = sin . (x + ((n * PI ) / 2))

then consider m being Element of 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:3
.= ((1 (#) (sin | Z)) `| Z) . x by NEWTON:15
.= ((sin | Z) `| Z) . x by RFUNCT_1:33
.= (sin `| Z) . x by A4, FDIFF_2:16
.= diff sin ,x by A4, A1, FDIFF_1:def 8
.= cos . x by SIN_COS:69
.= cos . (x + ((2 * PI ) * m)) by SIN_COS2:11
.= sin . ((x + ((i / 2) * PI )) + (PI / 2)) by A8, A9, SIN_COS:83
.= sin . (x + ((n * PI ) / 2)) ;
hence ((diff sin ,Z) . n) . x = sin . (x + ((n * PI ) / 2)) ; :: thesis: verum

end;

suppose not j is even ; :: thesis: ((diff sin ,Z) . n) . x = sin . (x + ((n * PI ) / 2))

then consider s being Element of NAT such that
A11: 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 A11, TAYLOR_2:19
.= (((((- 1) |^ (2 * s)) * (- 1)) (#) (sin | Z)) `| Z) . x by NEWTON:11
.= ((((1 |^ (2 * s)) * (- 1)) (#) (sin | Z)) `| Z) . x by WSIERP_1:3
.= (((1 * (- 1)) (#) (sin | Z)) `| Z) . x by NEWTON:15
.= (((- sin ) | Z) `| Z) . x by RFUNCT_1:65
.= (((- 1) (#) sin ) `| Z) . x by AA, FDIFF_2:16
.= (- 1) * (diff sin ,x) by A4, A1, A2, FDIFF_1:28
.= (- 1) * (cos . x) by SIN_COS:69
.= - (cos . x)
.= cos . (x + PI ) by SIN_COS:83
.= cos . ((x + PI ) + ((2 * PI ) * s)) by SIN_COS2:11
.= sin . ((x + ((i / 2) * PI )) + (PI / 2)) by A8, A11, SIN_COS:83
.= sin . (x + ((n * PI ) / 2)) ;
hence ((diff sin ,Z) . n) . x = sin . (x + ((n * PI ) / 2)) ; :: thesis: verum

end;

end;

end;

suppose not i is even ; :: thesis: ((diff sin ,Z) . n) . x = sin . (x + ((n * PI ) / 2))

then consider j being Element of NAT such that
A13: i = (2 * j) + 1 by ABIAN:9;

per cases ( j is even or not j is even ) ;

suppose j is even ; :: thesis: ((diff sin ,Z) . n) . x = sin . (x + ((n * PI ) / 2))

then consider m being Element of NAT such that
A14: j = 2 * m by ABIAN:def 2;
((diff sin ,Z) . (i + 1)) . x = (((diff sin ,Z) . ((2 * j) + 1)) `| Z) . x by A13, TAYLOR_1:def 5
.= ((((- 1) |^ (2 * m)) (#) (cos | Z)) `| Z) . x by A14, TAYLOR_2:19
.= (((1 |^ (2 * m)) (#) (cos | Z)) `| Z) . x by WSIERP_1:3
.= ((1 (#) (cos | Z)) `| Z) . x by NEWTON:15
.= ((cos | Z) `| Z) . x by RFUNCT_1:33
.= (cos `| Z) . x by A6, FDIFF_2:16
.= diff cos ,x by A6, A1, FDIFF_1:def 8
.= - (sin . x) by SIN_COS:68
.= sin . (x + PI ) by SIN_COS:83
.= sin . ((x + PI ) + ((2 * PI ) * m)) by SIN_COS2:10
.= sin . ((x + (((i - 1) / 2) * PI )) + PI ) by A13, A14
.= sin . (x + ((n * PI ) / 2)) ;
hence ((diff sin ,Z) . n) . x = sin . (x + ((n * PI ) / 2)) ; :: thesis: verum

end;

suppose not j is even ; :: thesis: ((diff sin ,Z) . n) . x = sin . (x + ((n * PI ) / 2))

then consider s being Element of NAT such that
A16: j = (2 * s) + 1 by ABIAN:9;
((diff sin ,Z) . (i + 1)) . x = (((diff sin ,Z) . ((2 * j) + 1)) `| Z) . x by A13, TAYLOR_1:def 5
.= ((((- 1) |^ j) (#) (cos | Z)) `| Z) . x by TAYLOR_2:19
.= (((((- 1) |^ (2 * s)) * (- 1)) (#) (cos | Z)) `| Z) . x by A16, NEWTON:11
.= ((((1 |^ (2 * s)) * (- 1)) (#) (cos | Z)) `| Z) . x by WSIERP_1:3
.= (((1 * (- 1)) (#) (cos | Z)) `| Z) . x by NEWTON:15
.= (((- cos ) | Z) `| Z) . x by RFUNCT_1:65
.= (((- 1) (#) cos ) `| Z) . x by AAA, FDIFF_2:16
.= (- 1) * (diff cos ,x) by A6, A1, A3, FDIFF_1:28
.= (- 1) * (- (sin . x)) by SIN_COS:68
.= sin . (x + ((2 * PI ) * s)) by SIN_COS2:10
.= sin . ((x + (((i - 3) / 2) * PI )) + (2 * PI )) by A13, A16, SIN_COS:83
.= 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 A18: n = 0 ; :: thesis: ((diff sin ,Z) . n) . x = sin . (x + ((n * PI ) / 2))

((diff sin ,Z) . n) . x = (sin | Z) . x by A18, TAYLOR_1:def 5
.= sin . (x + ((n * PI ) / 2)) by A18, A1, FUNCT_1:72 ;
hence ((diff sin ,Z) . n) . x = sin . (x + ((n * PI ) / 2)) ; :: thesis: verum

end;

end;