let n be Nat; for th being Real holds
( (Partial_Sums (th P_sin)) . n = (Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * n) + 1) & (Partial_Sums (th P_cos)) . n = (Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * n) )
let th be Real; ( (Partial_Sums (th P_sin)) . n = (Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * n) + 1) & (Partial_Sums (th P_cos)) . n = (Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * n) )
now for n being Nat holds S1[n]A1:
(Partial_Sums (th P_sin)) . 0 =
(th P_sin) . 0
by SERIES_1:def 1
.=
(((- 1) |^ 0) * (th |^ ((2 * 0) + 1))) / (((2 * 0) + 1) !)
by Def20
;
A2:
((2 * 0) + 1) ! =
(0 !) * 1
by NEWTON:15
.=
1
by NEWTON:12
;
A3:
(- 1) |^ 0 =
((- 1) GeoSeq) . 0
by PREPOWER:def 1
.=
1
by PREPOWER:3
;
A4:
(Partial_Sums (th P_cos)) . 0 =
(th P_cos) . 0
by SERIES_1:def 1
.=
(((- 1) |^ 0) * (th |^ (2 * 0))) / ((2 * 0) !)
by Def21
.=
(1 * ((th GeoSeq) . 0)) / 1
by A3, NEWTON:12, PREPOWER:def 1
.=
1
by PREPOWER:3
;
A5:
(
(Im ((th * <i>) ExpSeq)) . 0 = Im (((th * <i>) ExpSeq) . 0) &
(Im ((th * <i>) ExpSeq)) . 1
= Im (((th * <i>) ExpSeq) . 1) )
by COMSEQ_3:def 6;
A6:
th * <i> = 0 + (th * <i>)
;
A7:
(Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * 0) + 1) =
((Partial_Sums (Im ((th * <i>) ExpSeq))) . 0) + ((Im ((th * <i>) ExpSeq)) . 1)
by SERIES_1:def 1
.=
((Im ((th * <i>) ExpSeq)) . 0) + ((Im ((th * <i>) ExpSeq)) . 1)
by SERIES_1:def 1
.=
0 + (Im (((th * <i>) ExpSeq) . (0 + 1)))
by A5, Th3, COMPLEX1:6
.=
0 + (Im (((((th * <i>) ExpSeq) . 0) * (th * <i>)) / ((0 + 1) + (0 * <i>))))
by Th3
.=
Im ((1 * (th * <i>)) / 1)
by Th3
.=
th
by A6, COMPLEX1:12
;
defpred S1[
Nat]
means (
(Partial_Sums (th P_sin)) . $1
= (Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * $1) + 1) &
(Partial_Sums (th P_cos)) . $1
= (Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * $1) );
(Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * 0) =
(Re ((th * <i>) ExpSeq)) . 0
by SERIES_1:def 1
.=
Re (((th * <i>) ExpSeq) . 0)
by COMSEQ_3:def 5
.=
1
by Th3, COMPLEX1:6
;
then A8:
S1[
0 ]
by A1, A2, A3, A4, A7;
A9:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
thus
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A8, A9); verum end;
hence
( (Partial_Sums (th P_sin)) . n = (Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * n) + 1) & (Partial_Sums (th P_cos)) . n = (Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * n) )
; verum