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
A3: now :: thesis: for k being Nat holds (seq ^\ (K + 1)) . k >= 0
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) is summable by A1, SERIES_1:12;
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