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.|

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;(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

A4: now :: thesis: for n being Nat holds not |.seq.| . n <> 0

for n being Nat holds seq . n = 0c
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

end;then consider n1 being Nat such that

A5: |.seq.| . n1 <> 0 ;

A6: for n being Nat holds 0 <= (Partial_Sums |.seq.|) . n

proof

(Partial_Sums |.seq.|) . n1 > 0
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;|.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

proof

end;

hence
contradiction
by A2, A3; :: thesis: verumnow :: thesis: ( ( n1 = 0 & (Partial_Sums |.seq.|) . n1 > 0 ) or ( n1 <> 0 & (Partial_Sums |.seq.|) . n1 > 0 ) )end;

hence
(Partial_Sums |.seq.|) . n1 > 0
; :: thesis: verumper cases
( n1 = 0 or n1 <> 0 )
;

end;

case
n1 = 0
; :: thesis: (Partial_Sums |.seq.|) . n1 > 0

then
(Partial_Sums |.seq.|) . n1 <> 0
by A5, SERIES_1:def 1;

hence (Partial_Sums |.seq.|) . n1 > 0 by A6; :: thesis: verum

end;hence (Partial_Sums |.seq.|) . n1 > 0 by A6; :: thesis: verum

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;|.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

proof

hence
for n being Nat holds seq . n = 0c
; :: thesis: verum
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;0 = |.seq.| . n by A4

.= |.(seq . n).| by VALUED_1:18 ;

hence seq . n = 0c by COMPLEX1:45; :: thesis: verum