let Z be open Subset of REAL ; for n being Element of 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 Element of 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:34, SIN_COS:72;
defpred S1[ Element of 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:34, SIN_COS:73;
A3:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
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:65
.=
(((- 1) |^ k) * (- 1)) (#) (sin | Z)
by RFUNCT_1:29
.=
((- 1) |^ (k + 1)) (#) (sin | Z)
by NEWTON:11
;
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:65
.=
(((- 1) |^ (k + 1)) * (- 1)) (#) (sin | Z)
by RFUNCT_1:29
.=
((- 1) |^ ((k + 1) + 1)) (#) (sin | Z)
by NEWTON:11
;
(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:33
.=
((- 1) |^ 0 ) (#) (((- 1) (#) sin ) | Z)
by NEWTON:9
.=
((- 1) |^ 0 ) (#) ((- 1) (#) (sin | Z))
by RFUNCT_1:65
.=
(((- 1) |^ 0 ) * (- 1)) (#) (sin | Z)
by RFUNCT_1:29
.=
((- 1) |^ (0 + 1)) (#) (sin | Z)
by NEWTON:11
;
A11: (diff sin ,Z) . (2 * 0 ) =
sin | Z
by TAYLOR_1:def 5
.=
1 (#) (sin | Z)
by RFUNCT_1:33
.=
((- 1) |^ 0 ) (#) (sin | Z)
by NEWTON:9
;
A12: (diff cos ,Z) . (2 * 0 ) =
cos | Z
by TAYLOR_1:def 5
.=
1 (#) (cos | Z)
by RFUNCT_1:33
.=
((- 1) |^ 0 ) (#) (cos | Z)
by NEWTON:9
;
(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:33
.=
((- 1) |^ 0 ) (#) (cos | Z)
by NEWTON:9
;
then A13:
S1[ 0 ]
by A11, A12, A10;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(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