let Z be open Subset of REAL ; :: thesis: 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 ; :: 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:
sin is_differentiable_on Z
by FDIFF_1:34, SIN_COS:73;
A2:
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) );
A3:
S1[ 0 ]
proof
A4:
(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
;
A5:
(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 A1, FDIFF_2:16
.=
cos | Z
by Th17
.=
1
(#) (cos | Z)
by RFUNCT_1:33
.=
((- 1) |^ 0 ) (#) (cos | Z)
by NEWTON:9
;
A6:
(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 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 A2, 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
;
hence
S1[
0 ]
by A4, A5, A6;
:: thesis: verum
end;
A7:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A8:
S1[
k]
;
:: thesis: S1[k + 1]
A9:
(
sin | Z is_differentiable_on Z &
cos | Z is_differentiable_on Z )
by A1, A2, FDIFF_2:16;
A10:
(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 A8, A9, FDIFF_2:19
.=
((- 1) |^ k) (#) (cos `| Z)
by A2, 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
;
A11:
(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 A9, A10, FDIFF_2:19
.=
((- 1) |^ (k + 1)) (#) (sin `| Z)
by A1, FDIFF_2:16
.=
((- 1) |^ (k + 1)) (#) (cos | Z)
by Th17
;
A12:
(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 A8, A9, FDIFF_2:19
.=
((- 1) |^ (k + 1)) (#) (sin `| Z)
by A1, FDIFF_2:16
.=
((- 1) |^ (k + 1)) (#) (cos | Z)
by Th17
;
(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 A9, A12, FDIFF_2:19
.=
((- 1) |^ (k + 1)) (#) (cos `| Z)
by A2, 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
;
hence
S1[
k + 1]
by A10, A11, A12;
:: thesis: verum
end;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A3, A7);
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