for eps being real number st eps > 0 holds
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
dseq . n > (Sum eseq ) - eps
proof
let eps be
real number ;
:: thesis: ( eps > 0 implies ex N being Element of NAT st
for n being Element of NAT st n >= N holds
dseq . n > (Sum eseq ) - eps )
assume
eps > 0
;
:: thesis: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
dseq . n > (Sum eseq ) - eps
then A1:
eps / 2
> 0
by XREAL_1:141;
then consider K being
Element of
NAT such that A2:
(Partial_Sums eseq ) . K > (Sum eseq ) - (eps / 2)
by Th24, Th28;
deffunc H1(
Element of
NAT )
-> Element of
REAL =
(Partial_Sums (cseq $1)) . K;
consider dseqK being
Real_Sequence such that A3:
for
n being
Element of
NAT holds
dseqK . n = H1(
n)
from SEQ_1:sch 1();
(
dseqK is
convergent &
lim dseqK = (Partial_Sums eseq ) . K )
by A3, Th25;
then consider N being
Element of
NAT such that A4:
for
n being
Element of
NAT st
n >= N holds
dseqK . n > ((Partial_Sums eseq ) . K) - (eps / 2)
by A1, Th26;
take N1 =
N + 1;
:: thesis: for n being Element of NAT st n >= N1 holds
dseq . n > (Sum eseq ) - eps
let n be
Element of
NAT ;
:: thesis: ( n >= N1 implies dseq . n > (Sum eseq ) - eps )
assume A5:
n >= N1
;
:: thesis: dseq . n > (Sum eseq ) - eps
N + 1
>= N + 0
by XREAL_1:8;
then A6:
n >= N
by A5, XXREAL_0:2;
A7:
for
k being
Element of
NAT holds
(cseq n) . k >= 0
by A5, Th15;
cseq n is
summable
by A5, Th22;
then
Sum (cseq n) >= (Partial_Sums (cseq n)) . K
by A7, Th30;
then
dseq . n >= (Partial_Sums (cseq n)) . K
by A5, Th22;
then A8:
dseq . n >= dseqK . n
by A3;
dseqK . n > ((Partial_Sums eseq ) . K) - (eps / 2)
by A4, A6;
then A9:
dseq . n > ((Partial_Sums eseq ) . K) - (eps / 2)
by A8, XXREAL_0:2;
((Partial_Sums eseq ) . K) - (eps / 2) > ((Sum eseq ) - (eps / 2)) - (eps / 2)
by A2, XREAL_1:11;
hence
dseq . n > (Sum eseq ) - eps
by A9, XXREAL_0:2;
:: thesis: verum
end;
hence
( dseq is convergent & lim dseq = Sum eseq )
by Th27, Th29; :: thesis: verum