let seq be Complex_Sequence; :: thesis: ( seq is absolutely_summable & Sum |.seq.| = 0 implies for n being Nat holds seq . n = 0c )
assume that
A1: seq is absolutely_summable and
A2: Sum |.seq.| = 0 ; :: thesis: for n being Nat holds seq . n = 0c
A3: for n being Nat holds (Partial_Sums |.seq.|) . n <= Sum |.seq.|
proof
let n be Nat; :: thesis: (Partial_Sums |.seq.|) . n <= Sum |.seq.|
(Partial_Sums |.seq.|) . n <= lim (Partial_Sums |.seq.|) by A1, SEQ_4:37;
hence (Partial_Sums |.seq.|) . n <= Sum |.seq.| by SERIES_1:def 3; :: thesis: verum
end;
A4: now :: thesis: for n being Nat holds not |.seq.| . n <> 0
assume ex n being Nat st |.seq.| . n <> 0 ; :: thesis: contradiction
then consider n1 being Nat such that
A5: |.seq.| . n1 <> 0 ;
A6: for n being Nat holds 0 <= (Partial_Sums |.seq.|) . n
proof
let n be Nat; :: thesis: 0 <= (Partial_Sums |.seq.|) . n
|.seq.| . 0 = |.(seq . 0).| by VALUED_1:18;
then A7: 0 <= |.seq.| . 0 by COMPLEX1:46;
( n = n + 0 & (Partial_Sums |.seq.|) . 0 = |.seq.| . 0 ) by SERIES_1:def 1;
hence 0 <= (Partial_Sums |.seq.|) . n by A7, SEQM_3:5; :: thesis: verum
end;
(Partial_Sums |.seq.|) . n1 > 0
proof
now :: thesis: ( ( n1 = 0 & (Partial_Sums |.seq.|) . n1 > 0 ) or ( n1 <> 0 & (Partial_Sums |.seq.|) . n1 > 0 ) )
per cases ( n1 = 0 or n1 <> 0 ) ;
case A8: n1 <> 0 ; :: thesis: (Partial_Sums |.seq.|) . n1 > 0
set nn = n1 - 1;
|.seq.| . n1 = |.(seq . n1).| by VALUED_1:18;
then A9: ( (n1 - 1) + 1 = n1 & 0 <= |.seq.| . n1 ) by COMPLEX1:46;
0 + 1 <= n1 by A8, INT_1:7;
then A10: n1 - 1 in NAT by INT_1:5;
then 0 <= (Partial_Sums |.seq.|) . (n1 - 1) by A6;
then (|.seq.| . n1) + 0 <= (|.seq.| . n1) + ((Partial_Sums |.seq.|) . (n1 - 1)) by XREAL_1:7;
hence (Partial_Sums |.seq.|) . n1 > 0 by A5, A10, A9, SERIES_1:def 1; :: thesis: verum
end;
end;
end;
hence (Partial_Sums |.seq.|) . n1 > 0 ; :: thesis: verum
end;
hence contradiction by A2, A3; :: thesis: verum
end;
for n being Nat holds seq . n = 0c
proof
let n be Nat; :: thesis: seq . n = 0c
0 = |.seq.| . n by A4
.= |.(seq . n).| by VALUED_1:18 ;
hence seq . n = 0c by COMPLEX1:45; :: thesis: verum
end;
hence for n being Nat holds seq . n = 0c ; :: thesis: verum