let rseq be Real_Sequence; :: thesis: ( ( for n being Nat holds 0 <= rseq . n ) & rseq is summable & Sum rseq = 0 implies for n being Nat holds rseq . n = 0 )

assume that

A1: for n being Nat holds 0 <= rseq . n and

A2: rseq is summable and

A3: Sum rseq = 0 ; :: thesis: for n being Nat holds rseq . n = 0

A4: Partial_Sums rseq is bounded_above by A1, A2, SERIES_1:17;

A5: for n being Nat holds (Partial_Sums rseq) . n <= Sum rseq

assume that

A1: for n being Nat holds 0 <= rseq . n and

A2: rseq is summable and

A3: Sum rseq = 0 ; :: thesis: for n being Nat holds rseq . n = 0

A4: Partial_Sums rseq is bounded_above by A1, A2, SERIES_1:17;

A5: for n being Nat holds (Partial_Sums rseq) . n <= Sum rseq

proof

A6:
Partial_Sums rseq is V50()
by A1, SERIES_1:16;
let n be Nat; :: thesis: (Partial_Sums rseq) . n <= Sum rseq

(Partial_Sums rseq) . n <= lim (Partial_Sums rseq) by A1, A4, SEQ_4:37, SERIES_1:16;

hence (Partial_Sums rseq) . n <= Sum rseq by SERIES_1:def 3; :: thesis: verum

end;(Partial_Sums rseq) . n <= lim (Partial_Sums rseq) by A1, A4, SEQ_4:37, SERIES_1:16;

hence (Partial_Sums rseq) . n <= Sum rseq by SERIES_1:def 3; :: thesis: verum

now :: thesis: for n1 being Nat holds not rseq . n1 <> 0

hence
for n being Nat holds rseq . n = 0
; :: thesis: verumgiven n1 being Nat such that A7:
rseq . n1 <> 0
; :: thesis: contradiction

A8: for n being Nat holds 0 <= (Partial_Sums rseq) . n

end;A8: for n being Nat holds 0 <= (Partial_Sums rseq) . n

proof

(Partial_Sums rseq) . n1 > 0
let n be Nat; :: thesis: 0 <= (Partial_Sums rseq) . n

A9: ( n = n + 0 & (Partial_Sums rseq) . 0 = rseq . 0 ) by SERIES_1:def 1;

0 <= rseq . 0 by A1;

hence 0 <= (Partial_Sums rseq) . n by A6, A9, SEQM_3:5; :: thesis: verum

end;A9: ( n = n + 0 & (Partial_Sums rseq) . 0 = rseq . 0 ) by SERIES_1:def 1;

0 <= rseq . 0 by A1;

hence 0 <= (Partial_Sums rseq) . n by A6, A9, SEQM_3:5; :: thesis: verum

proof

end;

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

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

end;

case A10:
n1 = 0
; :: thesis: (Partial_Sums rseq) . n1 > 0

then
(Partial_Sums rseq) . n1 = rseq . 0
by SERIES_1:def 1;

hence (Partial_Sums rseq) . n1 > 0 by A1, A7, A10; :: thesis: verum

end;hence (Partial_Sums rseq) . n1 > 0 by A1, A7, A10; :: thesis: verum

case A11:
n1 <> 0
; :: thesis: (Partial_Sums rseq) . n1 > 0

set nn = n1 - 1;

A12: ( (n1 - 1) + 1 = n1 & 0 <= rseq . n1 ) by A1;

A13: n1 in NAT by ORDINAL1:def 12;

0 <= n1 by NAT_1:2;

then 0 + 1 <= n1 by A11, INT_1:7, A13;

then A14: n1 - 1 in NAT by INT_1:5, A13;

then A15: (Partial_Sums rseq) . ((n1 - 1) + 1) = ((Partial_Sums rseq) . (n1 - 1)) + (rseq . ((n1 - 1) + 1)) by SERIES_1:def 1;

0 <= (Partial_Sums rseq) . (n1 - 1) by A8, A14;

hence (Partial_Sums rseq) . n1 > 0 by A7, A12, A15; :: thesis: verum

end;A12: ( (n1 - 1) + 1 = n1 & 0 <= rseq . n1 ) by A1;

A13: n1 in NAT by ORDINAL1:def 12;

0 <= n1 by NAT_1:2;

then 0 + 1 <= n1 by A11, INT_1:7, A13;

then A14: n1 - 1 in NAT by INT_1:5, A13;

then A15: (Partial_Sums rseq) . ((n1 - 1) + 1) = ((Partial_Sums rseq) . (n1 - 1)) + (rseq . ((n1 - 1) + 1)) by SERIES_1:def 1;

0 <= (Partial_Sums rseq) . (n1 - 1) by A8, A14;

hence (Partial_Sums rseq) . n1 > 0 by A7, A12, A15; :: thesis: verum