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 ;
defpred S1[ 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 ;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
A5: cos | Z is_differentiable_on Z by ;
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
.= ((- 1) |^ k) (#) () by
.= ((- 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 ;
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
.= ((- 1) |^ (k + 1)) (#) () by
.= ((- 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
.= ((- 1) |^ (k + 1)) (#) () by
.= ((- 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
.= ((- 1) |^ (k + 1)) (#) () by
.= ((- 1) |^ (k + 1)) (#) (cos | Z) by Th17 ;
hence S1[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
.= () | Z by Th17
.= 1 (#) (() | 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
.= cos | Z by Th17
.= 1 (#) (cos | Z) by RFUNCT_1:21
.= ((- 1) |^ 0) (#) (cos | Z) by NEWTON:4 ;
then A13: S1[ 0 ] by ;
for n being Nat holds S1[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