let seq be Complex_Sequence; :: thesis: ( seq is absolutely_summable & Sum |.seq.| = 0 implies for n being Element of NAT holds seq . n = 0c )
assume that
A1: seq is absolutely_summable and
A2: Sum |.seq.| = 0 ; :: thesis: for n being Element of NAT holds seq . n = 0c
A3: for n being Element of NAT holds (Partial_Sums |.seq.|) . n <= Sum |.seq.|
proof
let n be Element of 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
assume ex n being Element of NAT st |.seq.| . n <> 0 ; :: thesis: contradiction
then consider n1 being Element of NAT such that
A5: |.seq.| . n1 <> 0 ;
A6: for n being Element of NAT holds 0 <= (Partial_Sums |.seq.|) . n
proof
let n be Element of 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
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 <= n1 by NAT_1:2;
then 0 + 1 <= n1 by A8, INT_1:7;
then A10: n1 - 1 is Element of 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 Element of NAT holds seq . n = 0c
proof
let n be Element of 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 Element of NAT holds seq . n = 0c ; :: thesis: verum