let Z be open Subset of REAL; :: thesis: for n being Nat holds
( (diff (sin,Z)) . (2 * n) = ((- 1) |^ n) (#) (sin | Z) & (diff (sin,Z)) . ((2 * n) + 1) = ((- 1) |^ n) (#) (cos | Z) & (diff (cos,Z)) . (2 * n) = ((- 1) |^ n) (#) (cos | Z) & (diff (cos,Z)) . ((2 * n) + 1) = ((- 1) |^ (n + 1)) (#) (sin | Z) )
let n be Nat; :: thesis: ( (diff (sin,Z)) . (2 * n) = ((- 1) |^ n) (#) (sin | Z) & (diff (sin,Z)) . ((2 * n) + 1) = ((- 1) |^ n) (#) (cos | Z) & (diff (cos,Z)) . (2 * n) = ((- 1) |^ n) (#) (cos | Z) & (diff (cos,Z)) . ((2 * n) + 1) = ((- 1) |^ (n + 1)) (#) (sin | Z) )
A1: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67;
defpred S₁[ Nat] means ( (diff (sin,Z)) . (2 * $1) = ((- 1) |^ $1) (#) (sin | Z) & (diff (sin,Z)) . ((2 * $1) + 1) = ((- 1) |^ $1) (#) (cos | Z) & (diff (cos,Z)) . (2 * $1) = ((- 1) |^ $1) (#) (cos | Z) & (diff (cos,Z)) . ((2 * $1) + 1) = ((- 1) |^ ($1 + 1)) (#) (sin | Z) );
A2: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
A5: cos | Z is_differentiable_on Z by A1, FDIFF_2:16;
A6: (diff (sin,Z)) . (2 * (k + 1)) = (diff (sin,Z)) . (((2 * k) + 1) + 1)
.= ((diff (sin,Z)) . ((2 * k) + 1)) `| Z by TAYLOR_1:def 5
.= ((- 1) |^ k) (#) ((cos | Z) `| Z) by A4, A5, FDIFF_2:19
.= ((- 1) |^ k) (#) (cos `| Z) by A1, FDIFF_2:16
.= ((- 1) |^ k) (#) (((- 1) (#) sin) | Z) by Th17
.= ((- 1) |^ k) (#) ((- 1) (#) (sin | Z)) by RFUNCT_1:49
.= (((- 1) |^ k) * (- 1)) (#) (sin | Z) by RFUNCT_1:17
.= ((- 1) |^ (k + 1)) (#) (sin | Z) by NEWTON:6 ;
A7: sin | Z is_differentiable_on Z by A2, FDIFF_2:16;
A8: (diff (cos,Z)) . (2 * (k + 1)) = (diff (cos,Z)) . (((2 * k) + 1) + 1)
.= ((diff (cos,Z)) . ((2 * k) + 1)) `| Z by TAYLOR_1:def 5
.= ((- 1) |^ (k + 1)) (#) ((sin | Z) `| Z) by A4, A7, FDIFF_2:19
.= ((- 1) |^ (k + 1)) (#) (sin `| Z) by A2, FDIFF_2:16
.= ((- 1) |^ (k + 1)) (#) (cos | Z) by Th17 ;
A9: (diff (cos,Z)) . ((2 * (k + 1)) + 1) = ((diff (cos,Z)) . (2 * (k + 1))) `| Z by TAYLOR_1:def 5
.= ((- 1) |^ (k + 1)) (#) ((cos | Z) `| Z) by A5, A8, FDIFF_2:19
.= ((- 1) |^ (k + 1)) (#) (cos `| Z) by A1, FDIFF_2:16
.= ((- 1) |^ (k + 1)) (#) (((- 1) (#) sin) | Z) by Th17
.= ((- 1) |^ (k + 1)) (#) ((- 1) (#) (sin | Z)) by RFUNCT_1:49
.= (((- 1) |^ (k + 1)) * (- 1)) (#) (sin | Z) by RFUNCT_1:17
.= ((- 1) |^ ((k + 1) + 1)) (#) (sin | Z) by NEWTON:6 ;
(diff (sin,Z)) . ((2 * (k + 1)) + 1) = ((diff (sin,Z)) . (2 * (k + 1))) `| Z by TAYLOR_1:def 5
.= ((- 1) |^ (k + 1)) (#) ((sin | Z) `| Z) by A7, A6, FDIFF_2:19
.= ((- 1) |^ (k + 1)) (#) (sin `| Z) by A2, FDIFF_2:16
.= ((- 1) |^ (k + 1)) (#) (cos | Z) by Th17 ;
hence S₁[k + 1] by A6, A8, A9; :: thesis: verum

end;

A10: (diff (cos,Z)) . ((2 * 0) + 1) = ((diff (cos,Z)) . 0) `| Z by TAYLOR_1:def 5
.= (cos | Z) `| Z by TAYLOR_1:def 5
.= cos `| Z by A1, FDIFF_2:16
.= (- sin) | Z by Th17
.= 1 (#) ((- sin) | Z) by RFUNCT_1:21
.= ((- 1) |^ 0) (#) (((- 1) (#) sin) | Z) by NEWTON:4
.= ((- 1) |^ 0) (#) ((- 1) (#) (sin | Z)) by RFUNCT_1:49
.= (((- 1) |^ 0) * (- 1)) (#) (sin | Z) by RFUNCT_1:17
.= ((- 1) |^ (0 + 1)) (#) (sin | Z) by NEWTON:6 ;
A11: (diff (sin,Z)) . (2 * 0) = sin | Z by TAYLOR_1:def 5
.= 1 (#) (sin | Z) by RFUNCT_1:21
.= ((- 1) |^ 0) (#) (sin | Z) by NEWTON:4 ;
A12: (diff (cos,Z)) . (2 * 0) = cos | Z by TAYLOR_1:def 5
.= 1 (#) (cos | Z) by RFUNCT_1:21
.= ((- 1) |^ 0) (#) (cos | Z) by NEWTON:4 ;
(diff (sin,Z)) . ((2 * 0) + 1) = ((diff (sin,Z)) . 0) `| Z by TAYLOR_1:def 5
.= (sin | Z) `| Z by TAYLOR_1:def 5
.= sin `| Z by A2, FDIFF_2:16
.= cos | Z by Th17
.= 1 (#) (cos | Z) by RFUNCT_1:21
.= ((- 1) |^ 0) (#) (cos | Z) by NEWTON:4 ;
then A13: S₁[ 0 ] by A11, A12, A10;
for n being Nat holds S₁[n] from NAT_1:sch 2(A13, A3);
hence ( (diff (sin,Z)) . (2 * n) = ((- 1) |^ n) (#) (sin | Z) & (diff (sin,Z)) . ((2 * n) + 1) = ((- 1) |^ n) (#) (cos | Z) & (diff (cos,Z)) . (2 * n) = ((- 1) |^ n) (#) (cos | Z) & (diff (cos,Z)) . ((2 * n) + 1) = ((- 1) |^ (n + 1)) (#) (sin | Z) ) ; :: thesis: verum