let Z be open Subset of REAL; 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; ( (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 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 FDIFF_1:26, SIN_COS:68;
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[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
S1[
k + 1]
by A6, A8, A9;
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:
S1[ 0 ]
by A11, A12, A10;
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) )
; verum