let f be nonnegative-yielding Real_Sequence; :: thesis: ( f is summable implies for p being Real st p > 0 holds
ex i being Element of NAT st Sum (f ^\ i) < p )
assume A1: f is summable ; :: thesis: for p being Real st p > 0 holds
ex i being Element of NAT st Sum (f ^\ i) < p
let p be Real; :: thesis: ( p > 0 implies ex i being Element of NAT st Sum (f ^\ i) < p )
assume B1: p > 0 ; :: thesis: ex i being Element of NAT st Sum (f ^\ i) < p
assume O1: for i being Element of NAT holds Sum (f ^\ i) >= p ; :: thesis: contradiction
set S = Sum f;
Partial_Sums f is convergent by A1, SERIES_1:def 2;
then consider n being Nat such that
D1: for m being Nat st n <= m holds
|.(((Partial_Sums f) . m) - (Sum f)).| < p by B1, SEQ_2:def 7;
reconsider m = n + 1 as Element of NAT ;
reconsider m1 = m + 1 as Element of NAT ;
x1: ((Partial_Sums f) . m) + (Sum (f ^\ m1)) = Sum f by A1, SERIES_1:15;
set R = f ^\ m1;
Y1: f ^\ m1 is summable by A1, SERIES_1:12;
for n being Nat holds 0 <= (f ^\ m1) . n by RINFSUP1:def 3;
then Sum (f ^\ m1) >= 0 by Y1, SERIES_1:18;
then - ((Sum f) - ((Partial_Sums f) . m)) <= - 0 by x1;
per cases then ( ((Partial_Sums f) . m) - (Sum f) < 0 or ((Partial_Sums f) . m) - (Sum f) = 0 ) ;
suppose X3: ((Partial_Sums f) . m) - (Sum f) < 0 ; :: thesis: contradiction
|.(((Partial_Sums f) . m) - (Sum f)).| < p by D1, NAT_1:11;
then - (((Partial_Sums f) . m) - (Sum f)) < p by X3, ABSVALUE:def 1;
hence contradiction by O1, x1; :: thesis: verum
end;
suppose ((Partial_Sums f) . m) - (Sum f) = 0 ; :: thesis: contradiction
hence contradiction by O1, x1, B1; :: thesis: verum
end;
end;