for eps being Real st eps > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
dseq . n > (Sum eseq) - eps
proof
let eps be
Real;
( eps > 0 implies ex N being Nat st
for n being Nat st n >= N holds
dseq . n > (Sum eseq) - eps )
assume A1:
eps > 0
;
ex N being Nat st
for n being Nat st n >= N holds
dseq . n > (Sum eseq) - eps
then consider K being
Nat such that A2:
(Partial_Sums eseq) . K > (Sum eseq) - (eps / 2)
by Th23, Th27, XREAL_1:139;
A3:
((Partial_Sums eseq) . K) - (eps / 2) > ((Sum eseq) - (eps / 2)) - (eps / 2)
by A2, XREAL_1:9;
deffunc H1(
Nat)
-> set =
(Partial_Sums (cseq $1)) . K;
consider dseqK being
Real_Sequence such that A4:
for
n being
Nat holds
dseqK . n = H1(
n)
from SEQ_1:sch 1();
(
dseqK is
convergent &
lim dseqK = (Partial_Sums eseq) . K )
by A4, Th24;
then consider N being
Nat such that A5:
for
n being
Nat st
n >= N holds
dseqK . n > ((Partial_Sums eseq) . K) - (eps / 2)
by A1, Th25, XREAL_1:139;
take N1 =
N + 1;
for n being Nat st n >= N1 holds
dseq . n > (Sum eseq) - eps
let n be
Nat;
( n >= N1 implies dseq . n > (Sum eseq) - eps )
assume A6:
n >= N1
;
dseq . n > (Sum eseq) - eps
then
( ( for
k being
Nat holds
(cseq n) . k >= 0 ) &
cseq n is
summable )
by Th14, Th21;
then
Sum (cseq n) >= (Partial_Sums (cseq n)) . K
by Th29;
then
dseq . n >= (Partial_Sums (cseq n)) . K
by A6, Th21;
then A7:
dseq . n >= dseqK . n
by A4;
N + 1
>= N + 0
by XREAL_1:6;
then
n >= N
by A6, XXREAL_0:2;
then
dseqK . n > ((Partial_Sums eseq) . K) - (eps / 2)
by A5;
then
dseq . n > ((Partial_Sums eseq) . K) - (eps / 2)
by A7, XXREAL_0:2;
hence
dseq . n > (Sum eseq) - eps
by A3, XXREAL_0:2;
verum
end;
hence
( dseq is convergent & lim dseq = Sum eseq )
by Th26, Th28; verum