let seq be Complex_Sequence; :: thesis: for n being Nat st ( for i being Nat holds
( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ) holds
|.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n
let n be Nat; :: thesis: ( ( for i being Nat holds
( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ) implies |.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n )
defpred S1[ Nat] means |.(Partial_Sums seq).| . $1 = (Partial_Sums |.seq.|) . $1;
assume A1: for i being Nat holds
( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ; :: thesis: |.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n
A2: now :: thesis: for m being Nat st S1[m] holds
S1[m + 1]
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A3: S1[m] ; :: thesis: S1[m + 1]
thus S1[m + 1] :: thesis: verum
proof
for i being Nat holds (Partial_Sums (Re seq)) . i >= 0
proof
defpred S2[ Nat] means (Partial_Sums (Re seq)) . $1 >= 0 ;
let i be Nat; :: thesis: (Partial_Sums (Re seq)) . i >= 0
A4: now :: thesis: for k being Nat st S2[k] holds
S2[k + 1]
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A5: S2[k] ; :: thesis: S2[k + 1]
( (Partial_Sums (Re seq)) . (k + 1) = ((Partial_Sums (Re seq)) . k) + ((Re seq) . (k + 1)) & (Re seq) . (k + 1) >= 0 ) by A1, SERIES_1:def 1;
then (Partial_Sums (Re seq)) . (k + 1) >= 0 + 0 by A5;
hence S2[k + 1] ; :: thesis: verum
end;
(Partial_Sums (Re seq)) . 0 = (Re seq) . 0 by SERIES_1:def 1;
then A6: S2[ 0 ] by A1;
for i being Nat holds S2[i] from NAT_1:sch 2(A6, A4);
 hence (Partial_Sums (Re seq)) . i >= 0 ; :: thesis: verum
end;
then (Partial_Sums (Re seq)) . m >= 0 ;
then (Re (Partial_Sums seq)) . m >= 0 by COMSEQ_3:26;
then A7: Re ((Partial_Sums seq) . m) >= 0 by COMSEQ_3:def 5;
set z2 = seq . (m + 1);
set z1 = (Partial_Sums seq) . m;
A8: |.(Partial_Sums seq).| . (m + 1) = |.((Partial_Sums seq) . (m + 1)).| by VALUED_1:18
.= |.(((Partial_Sums seq) . m) + (seq . (m + 1))).| by SERIES_1:def 1 ;
for i being Nat holds (Partial_Sums (Im seq)) . i = 0
proof
defpred S2[ Nat] means (Partial_Sums (Im seq)) . $1 = 0 ;
let i be Nat; :: thesis: (Partial_Sums (Im seq)) . i = 0
A9: now :: thesis: for k being Nat st S2[k] holds
S2[k + 1]
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
A10: (Partial_Sums (Im seq)) . (k + 1) = ((Partial_Sums (Im seq)) . k) + ((Im seq) . (k + 1)) by SERIES_1:def 1;
assume S2[k] ; :: thesis: S2[k + 1]
hence S2[k + 1] by A1, A10; :: thesis: verum
end;
(Partial_Sums (Im seq)) . 0 = (Im seq) . 0 by SERIES_1:def 1;
then A11: S2[ 0 ] by A1;
for i being Nat holds S2[i] from NAT_1:sch 2(A11, A9);
 hence (Partial_Sums (Im seq)) . i = 0 ; :: thesis: verum
end;
then (Partial_Sums (Im seq)) . m = 0 ;
then (Im (Partial_Sums seq)) . m = 0 by COMSEQ_3:26;
then A12: Im ((Partial_Sums seq) . m) = 0 by COMSEQ_3:def 6;
(Im seq) . (m + 1) = 0 by A1;
then Im (seq . (m + 1)) = 0 by COMSEQ_3:def 6;
then A13: (Re ((Partial_Sums seq) . m)) * (Im (seq . (m + 1))) = (Re (seq . (m + 1))) * (Im ((Partial_Sums seq) . m)) by A12;
(Re seq) . (m + 1) >= 0 by A1;
then Re (seq . (m + 1)) >= 0 by COMSEQ_3:def 5;
then ((Re ((Partial_Sums seq) . m)) * (Re (seq . (m + 1)))) + ((Im ((Partial_Sums seq) . m)) * (Im (seq . (m + 1)))) >= 0 by A7, A12;
then |.(Partial_Sums seq).| . (m + 1) = |.((Partial_Sums seq) . m).| + |.(seq . (m + 1)).| by A8, A13, Lm3
.= (|.(Partial_Sums seq).| . m) + |.(seq . (m + 1)).| by VALUED_1:18
.= ((Partial_Sums |.seq.|) . m) + (|.seq.| . (m + 1)) by A3, VALUED_1:18 ;
hence S1[m + 1] by SERIES_1:def 1; :: thesis: verum
end;
end;
|.(Partial_Sums seq).| . 0 = |.((Partial_Sums seq) . 0).| by VALUED_1:18
.= |.(seq . 0).| by SERIES_1:def 1
.= |.seq.| . 0 by VALUED_1:18 ;
then A14: S1[ 0 ] by SERIES_1:def 1;
for m being Nat holds S1[m] from NAT_1:sch 2(A14, A2);
 hence |.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n ; :: thesis: verum