let K be Nat; :: thesis: for seq being Real_Sequence st seq is summable & ( for k being Nat holds seq . k >= 0 ) holds

Sum seq >= (Partial_Sums seq) . K

let seq be Real_Sequence; :: thesis: ( seq is summable & ( for k being Nat holds seq . k >= 0 ) implies Sum seq >= (Partial_Sums seq) . K )

assume that

A1: seq is summable and

A2: for k being Nat holds seq . k >= 0 ; :: thesis: Sum seq >= (Partial_Sums seq) . K

then Sum (seq ^\ (K + 1)) >= 0 by A3, SERIES_1:18;

then ((Partial_Sums seq) . K) + (Sum (seq ^\ (K + 1))) >= ((Partial_Sums seq) . K) + 0 by XREAL_1:6;

hence Sum seq >= (Partial_Sums seq) . K by A1, SERIES_1:15; :: thesis: verum

Sum seq >= (Partial_Sums seq) . K

let seq be Real_Sequence; :: thesis: ( seq is summable & ( for k being Nat holds seq . k >= 0 ) implies Sum seq >= (Partial_Sums seq) . K )

assume that

A1: seq is summable and

A2: for k being Nat holds seq . k >= 0 ; :: thesis: Sum seq >= (Partial_Sums seq) . K

A3: now :: thesis: for k being Nat holds (seq ^\ (K + 1)) . k >= 0

seq ^\ (K + 1) is summable
by A1, SERIES_1:12;let k be Nat; :: thesis: (seq ^\ (K + 1)) . k >= 0

(seq ^\ (K + 1)) . k = seq . ((K + 1) + k) by NAT_1:def 3;

hence (seq ^\ (K + 1)) . k >= 0 by A2; :: thesis: verum

end;(seq ^\ (K + 1)) . k = seq . ((K + 1) + k) by NAT_1:def 3;

hence (seq ^\ (K + 1)) . k >= 0 by A2; :: thesis: verum

then Sum (seq ^\ (K + 1)) >= 0 by A3, SERIES_1:18;

then ((Partial_Sums seq) . K) + (Sum (seq ^\ (K + 1))) >= ((Partial_Sums seq) . K) + 0 by XREAL_1:6;

hence Sum seq >= (Partial_Sums seq) . K by A1, SERIES_1:15; :: thesis: verum