let n be Element of NAT ; :: thesis: 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; :: thesis: ( (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

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 Def24 ;
A2: th |^ ((2 * 0) + 1) = (th GeoSeq) . (0 + 1) by PREPOWER:def 1
.= ((th GeoSeq) . 0) * th by PREPOWER:3
.= 1 * th by PREPOWER:3
.= th ;
A3: ((2 * 0) + 1) ! = (0 !) * 1 by NEWTON:15
.= 1 by NEWTON:12 ;
A4: (- 1) |^ 0 = ((- 1) GeoSeq) . 0 by PREPOWER:def 1
.= 1 by PREPOWER:3 ;
A5: (Partial_Sums (th P_cos)) . 0 = (th P_cos) . 0 by SERIES_1:def 1
.= (((- 1) |^ 0) * (th |^ (2 * 0))) / ((2 * 0) !) by Def25
.= (1 * ((th GeoSeq) . 0)) / 1 by A4, NEWTON:12, PREPOWER:def 1
.= 1 by PREPOWER:3 ;
A6: ( (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;
A7: th * <i> = 0 + (th * <i>) ;
A8: (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 A6, Th4, COMPLEX1:6
.= 0 + (Im (((((th * <i>) ExpSeq) . 0) * (th * <i>)) / ((0 + 1) + (0 * <i>)))) by Th4
.= Im ((1 * (th * <i>)) / 1) by Th4
.= th by A7, COMPLEX1:12 ;
defpred S₁[ Element of 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 Th4, COMPLEX1:6 ;
then A9: S₁[ 0 ] by A1, A2, A3, A4, A5, A8;
A10: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A11: (Partial_Sums (th P_sin)) . k = (Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * k) + 1) and
A12: (Partial_Sums (th P_cos)) . k = (Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * k) ; :: thesis: S₁[k + 1]
(Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * (k + 1)) + 1) = ((Partial_Sums (Im ((th * <i>) ExpSeq))) . (((2 * k) + 1) + 1)) + ((Im ((th * <i>) ExpSeq)) . ((2 * (k + 1)) + 1)) by SERIES_1:def 1
.= (((Partial_Sums (th P_sin)) . k) + ((Im ((th * <i>) ExpSeq)) . (2 * (k + 1)))) + ((Im ((th * <i>) ExpSeq)) . ((2 * (k + 1)) + 1)) by A11, SERIES_1:def 1
.= (((Partial_Sums (th P_sin)) . k) + (Im (((th * <i>) ExpSeq) . (2 * (k + 1))))) + ((Im ((th * <i>) ExpSeq)) . ((2 * (k + 1)) + 1)) by COMSEQ_3:def 6
.= (((Partial_Sums (th P_sin)) . k) + (Im (((th * <i>) ExpSeq) . (2 * (k + 1))))) + (Im (((th * <i>) ExpSeq) . ((2 * (k + 1)) + 1))) by COMSEQ_3:def 6
.= (((Partial_Sums (th P_sin)) . k) + (Im (((th * <i>) |^ (2 * (k + 1))) / ((2 * (k + 1)) !)))) + (Im (((th * <i>) ExpSeq) . ((2 * (k + 1)) + 1))) by Def8
.= (((Partial_Sums (th P_sin)) . k) + (Im (((th * <i>) |^ (2 * (k + 1))) / ((2 * (k + 1)) !)))) + (Im (((th * <i>) |^ ((2 * (k + 1)) + 1)) / (((2 * (k + 1)) + 1) !))) by Def8
.= (((Partial_Sums (th P_sin)) . k) + (Im ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !)))) + (Im (((th * <i>) |^ ((2 * (k + 1)) + 1)) / (((2 * (k + 1)) + 1) !))) by Th36
.= (((Partial_Sums (th P_sin)) . k) + (Im ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !)))) + (Im (((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) * <i>) / (((2 * (k + 1)) + 1) !))) by Th36 ;
then (Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * (k + 1)) + 1) = (((Partial_Sums (th P_sin)) . k) + (Im (((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !)) + ((0 / ((2 * (k + 1)) !)) * <i>)))) + (Im (((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) * <i>) / (((2 * (k + 1)) + 1) !))) ;
then (Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * (k + 1)) + 1) = (((Partial_Sums (th P_sin)) . k) + 0) + (Im ((0 / (((2 * (k + 1)) + 1) !)) + (((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) / (((2 * (k + 1)) + 1) !)) * <i>))) by COMPLEX1:12
.= (((Partial_Sums (th P_sin)) . k) + (0 / ((2 * (k + 1)) !))) + ((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) / (((2 * (k + 1)) + 1) !)) by COMPLEX1:12 ;
then A13: (Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * (k + 1)) + 1) = ((Partial_Sums (th P_sin)) . k) + ((th P_sin) . (k + 1)) by Def24
.= (Partial_Sums (th P_sin)) . (k + 1) by SERIES_1:def 1 ;
(Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * (k + 1)) = ((Partial_Sums (Re ((th * <i>) ExpSeq))) . ((2 * k) + 1)) + ((Re ((th * <i>) ExpSeq)) . (((2 * k) + 1) + 1)) by SERIES_1:def 1
.= (((Partial_Sums (th P_cos)) . k) + ((Re ((th * <i>) ExpSeq)) . ((2 * k) + 1))) + ((Re ((th * <i>) ExpSeq)) . (((2 * k) + 1) + 1)) by A12, SERIES_1:def 1
.= (((Partial_Sums (th P_cos)) . k) + (Re (((th * <i>) ExpSeq) . ((2 * k) + 1)))) + ((Re ((th * <i>) ExpSeq)) . (((2 * k) + 1) + 1)) by COMSEQ_3:def 5
.= (((Partial_Sums (th P_cos)) . k) + (Re (((th * <i>) ExpSeq) . ((2 * k) + 1)))) + (Re (((th * <i>) ExpSeq) . (((2 * k) + 1) + 1))) by COMSEQ_3:def 5
.= (((Partial_Sums (th P_cos)) . k) + (Re (((th * <i>) |^ ((2 * k) + 1)) / (((2 * k) + 1) !)))) + (Re (((th * <i>) ExpSeq) . (((2 * k) + 1) + 1))) by Def8
.= (((Partial_Sums (th P_cos)) . k) + (Re (((th * <i>) |^ ((2 * k) + 1)) / (((2 * k) + 1) !)))) + (Re (((th * <i>) |^ (2 * (k + 1))) / ((((2 * k) + 1) + 1) !))) by Def8
.= (((Partial_Sums (th P_cos)) . k) + (Re (((((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i>) / (((2 * k) + 1) !)))) + (Re (((th * <i>) |^ (2 * (k + 1))) / ((2 * (k + 1)) !))) by Th36
.= (((Partial_Sums (th P_cos)) . k) + (Re (((((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i>) / (((2 * k) + 1) !)))) + (Re ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !))) by Th36 ;
then (Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * (k + 1)) = (((Partial_Sums (th P_cos)) . k) + (Re ((0 / (((2 * k) + 1) !)) + (((((- 1) |^ k) * (th |^ ((2 * k) + 1))) / (((2 * k) + 1) !)) * <i>)))) + (Re ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !))) ;
then (Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * (k + 1)) = (((Partial_Sums (th P_cos)) . k) + (0 / (((2 * k) + 1) !))) + (Re (((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !)) + ((0 / ((2 * (k + 1)) !)) * <i>))) by COMPLEX1:12
.= (((Partial_Sums (th P_cos)) . k) + (0 / (((2 * k) + 1) !))) + ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !)) by COMPLEX1:12 ;
then (Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * (k + 1)) = ((Partial_Sums (th P_cos)) . k) + ((th P_cos) . (k + 1)) by Def25
.= (Partial_Sums (th P_cos)) . (k + 1) by SERIES_1:def 1 ;
hence S₁[k + 1] by A13; :: thesis: verum

end;

thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A9, A10); :: thesis: 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) ) ; :: thesis: verum