let seq1 be Real_Sequence; :: thesis: ( seq1 is summable implies ex r being Real st
( 0 < r & ( for k being Nat holds |.(Sum (seq1 ^\ k)).| < r ) ) )
assume A1: seq1 is summable ; :: thesis: ex r being Real st
( 0 < r & ( for k being Nat holds |.(Sum (seq1 ^\ k)).| < r ) )
defpred S1[ Nat] means ex r being Real st
( r >= 0 & ( for i being Nat st i <= $1 holds
|.(Sum (seq1 ^\ i)).| <= r ) );
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[k + 1]
then consider r being Real such that
A3: r >= 0 and
A4: for i being Nat st i <= k holds
|.(Sum (seq1 ^\ i)).| <= r ;
take M = max (r,|.(Sum (seq1 ^\ (k + 1))).|); :: thesis: ( M >= 0 & ( for i being Nat st i <= k + 1 holds
|.(Sum (seq1 ^\ i)).| <= M ) )
thus M >= 0 by A3, XXREAL_0:25; :: thesis: for i being Nat st i <= k + 1 holds
|.(Sum (seq1 ^\ i)).| <= M
let i be Nat; :: thesis: ( i <= k + 1 implies |.(Sum (seq1 ^\ i)).| <= M )
assume A5: i <= k + 1 ; :: thesis: |.(Sum (seq1 ^\ i)).| <= M
now :: thesis: |.(Sum (seq1 ^\ i)).| <= M
per cases ( i = k + 1 or i <= k ) by A5, NAT_1:8;
suppose i = k + 1 ; :: thesis: |.(Sum (seq1 ^\ i)).| <= M
hence |.(Sum (seq1 ^\ i)).| <= M by XXREAL_0:25; :: thesis: verum
end;
suppose A6: i <= k ; :: thesis: |.(Sum (seq1 ^\ i)).| <= M
A7: r <= M by XXREAL_0:25;
|.(Sum (seq1 ^\ i)).| <= r by A4, A6;
hence |.(Sum (seq1 ^\ i)).| <= M by A7, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence |.(Sum (seq1 ^\ i)).| <= M ; :: thesis: verum
end;
set P = Partial_Sums seq1;
A8: lim (Partial_Sums seq1) = Sum seq1 by SERIES_1:def 3;
Partial_Sums seq1 is convergent by A1, SERIES_1:def 2;
then consider n being Nat such that
A9: for m being Nat st n <= m holds
|.(((Partial_Sums seq1) . m) - (Sum seq1)).| < 1 by A8, SEQ_2:def 7;
A10: S1[ 0 ]
proof
take |.(Sum seq1).| ; :: thesis: ( |.(Sum seq1).| >= 0 & ( for i being Nat st i <= 0 holds
|.(Sum (seq1 ^\ i)).| <= |.(Sum seq1).| ) )
thus |.(Sum seq1).| >= 0 by COMPLEX1:46; :: thesis: for i being Nat st i <= 0 holds
|.(Sum (seq1 ^\ i)).| <= |.(Sum seq1).|
let i be Nat; :: thesis: ( i <= 0 implies |.(Sum (seq1 ^\ i)).| <= |.(Sum seq1).| )
assume i <= 0 ; :: thesis: |.(Sum (seq1 ^\ i)).| <= |.(Sum seq1).|
then i = 0 ;
hence |.(Sum (seq1 ^\ i)).| <= |.(Sum seq1).| by NAT_1:47; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A10, A2);
 then consider r being Real such that
A11: r >= 0 and
A12: for i being Nat st i <= n holds
|.(Sum (seq1 ^\ i)).| <= r ;
take r1 = r + 1; :: thesis: ( 0 < r1 & ( for k being Nat holds |.(Sum (seq1 ^\ k)).| < r1 ) )
thus r1 > 0 by A11; :: thesis: for k being Nat holds |.(Sum (seq1 ^\ k)).| < r1
let k be Nat; :: thesis: |.(Sum (seq1 ^\ k)).| < r1
now :: thesis: |.(Sum (seq1 ^\ k)).| < r1
per cases ( k <= n or k > n ) ;
suppose A13: k <= n ; :: thesis: |.(Sum (seq1 ^\ k)).| < r1
A14: 0 + r < r1 by XREAL_1:8;
|.(Sum (seq1 ^\ k)).| <= r by A12, A13;
hence |.(Sum (seq1 ^\ k)).| < r1 by A14, XXREAL_0:2; :: thesis: verum
end;
suppose A15: k > n ; :: thesis: |.(Sum (seq1 ^\ k)).| < r1
then reconsider k1 = k - 1 as Nat by NAT_1:20;
k1 + 1 > n by A15;
then k1 >= n by NAT_1:13;
then A16: |.(((Partial_Sums seq1) . k1) - (Sum seq1)).| < 1 by A9;
Sum seq1 = ((Partial_Sums seq1) . k1) + (Sum (seq1 ^\ (k1 + 1))) by A1, SERIES_1:15;
then |.(- (Sum (seq1 ^\ (k1 + 1)))).| < 1 by A16;
then A17: |.(Sum (seq1 ^\ (k1 + 1))).| < 1 by COMPLEX1:52;
1 + 0 <= r1 by A11, XREAL_1:6;
hence |.(Sum (seq1 ^\ k)).| < r1 by A17, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence |.(Sum (seq1 ^\ k)).| < r1 ; :: thesis: verum