let a be Real_Sequence; ( a is nonnegative-yielding & a is non-increasing & a is convergent & lim a = 0 implies ( alternating_series a is summable & ( for n being Nat holds
( (Partial_Sums (alternating_series a)) . (2 * n) >= Sum (alternating_series a) & Sum (alternating_series a) >= (Partial_Sums (alternating_series a)) . ((2 * n) + 1) ) ) ) )
assume A1:
( a is nonnegative-yielding & a is non-increasing & a is convergent & lim a = 0 )
; ( alternating_series a is summable & ( for n being Nat holds
( (Partial_Sums (alternating_series a)) . (2 * n) >= Sum (alternating_series a) & Sum (alternating_series a) >= (Partial_Sums (alternating_series a)) . ((2 * n) + 1) ) ) )
set A = alternating_series a;
set P = Partial_Sums (alternating_series a);
defpred S1[ Nat, object ] means $2 = (Partial_Sums (alternating_series a)) . (2 * $1);
defpred S2[ Nat, object ] means $2 = (Partial_Sums (alternating_series a)) . ((2 * $1) + 1);
A2:
for x being Element of NAT ex y being Element of REAL st S1[x,y]
;
A3:
for x being Element of NAT ex y being Element of REAL st S2[x,y]
;
consider Sp being Function of NAT,REAL such that
A4:
for x being Element of NAT holds S1[x,Sp . x]
from FUNCT_2:sch 3(A2);
consider Sn being Function of NAT,REAL such that
A5:
for x being Element of NAT holds S2[x,Sn . x]
from FUNCT_2:sch 3(A3);
A6:
for n being Nat holds Sn . n <= Sn . (n + 1)
then A11:
Sn is non-decreasing
by VALUED_1:def 15;
A12:
for n being Nat holds Sp . n >= Sp . (n + 1)
then A17:
Sp is non-increasing
by VALUED_1:def 16;
A18:
for n being Nat holds Sp . n >= Sn . n
for n being Nat holds Sp . n > (Sn . 0) - 1
then A21:
Sp is bounded_below
by SEQ_2:def 4;
A22:
for n being Nat holds Sn . n < (Sp . 0) + 1
then A23:
Sn is bounded_above
by SEQ_2:def 3;
deffunc H1( Nat) -> Element of NAT = (2 * $1) + 1;
A24:
for x being Element of NAT holds H1(x) in NAT
;
consider Double being Function of NAT,NAT such that
A25:
for x being Element of NAT holds Double . x = H1(x)
from FUNCT_2:sch 8(A24);
reconsider Double1 = Double as ManySortedSet of NAT ;
for n being Nat holds Double . n < Double . (n + 1)
then A27:
Double1 is increasing sequence of NAT
by VALUED_1:def 13;
A28:
rng (a * Double1) c= REAL
;
( rng Double c= NAT & dom a = NAT & dom Double = NAT )
by FUNCT_2:def 1;
then A29:
dom (a * Double1) = NAT
by RELAT_1:27;
then reconsider aD = a * Double1 as Real_Sequence by A28, FUNCT_2:2;
reconsider aD = aD as subsequence of a by VALUED_0:def 17, A27;
A30:
( aD is convergent & lim aD = 0 )
by SEQ_4:16, SEQ_4:17, A1;
A31:
( Sp - Sn is convergent & lim (Sp - Sn) = (lim Sp) - (lim Sn) )
by A21, A17, A23, A11, SEQ_2:12;
for x being object st x in NAT holds
aD . x = (Sp - Sn) . x
then A36:
aD = Sp - Sn
;
A37:
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums (alternating_series a)) . m) - (lim Sp)).| < p
proof
let p be
Real;
( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums (alternating_series a)) . m) - (lim Sp)).| < p )
assume A38:
0 < p
;
ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums (alternating_series a)) . m) - (lim Sp)).| < p
consider n1 being
Nat such that A39:
for
m being
Nat st
n1 <= m holds
|.((Sp . m) - (lim Sp)).| < p
by A38, A21, A17, SEQ_2:def 7;
consider n2 being
Nat such that A40:
for
m being
Nat st
n2 <= m holds
|.((Sn . m) - (lim Sp)).| < p
by A38, A23, A11, SEQ_2:def 7, A36, A30, A31;
set N =
max (
(2 * n1),
((2 * n2) + 1));
reconsider N =
max (
(2 * n1),
((2 * n2) + 1)) as
Nat by XXREAL_0:def 10;
take
N
;
for m being Nat st N <= m holds
|.(((Partial_Sums (alternating_series a)) . m) - (lim Sp)).| < p
let m be
Nat;
( N <= m implies |.(((Partial_Sums (alternating_series a)) . m) - (lim Sp)).| < p )
assume A41:
N <= m
;
|.(((Partial_Sums (alternating_series a)) . m) - (lim Sp)).| < p
end;
hence
alternating_series a is summable
by SERIES_1:def 2, SEQ_2:def 6; for n being Nat holds
( (Partial_Sums (alternating_series a)) . (2 * n) >= Sum (alternating_series a) & Sum (alternating_series a) >= (Partial_Sums (alternating_series a)) . ((2 * n) + 1) )
let n be Nat; ( (Partial_Sums (alternating_series a)) . (2 * n) >= Sum (alternating_series a) & Sum (alternating_series a) >= (Partial_Sums (alternating_series a)) . ((2 * n) + 1) )
n in NAT
by ORDINAL1:def 12;
then A46:
( Sp . n = (Partial_Sums (alternating_series a)) . (2 * n) & Sn . n = (Partial_Sums (alternating_series a)) . ((2 * n) + 1) )
by A4, A5;
Partial_Sums (alternating_series a) is convergent
by A37, SEQ_2:def 6;
then
( lim (Partial_Sums (alternating_series a)) = lim Sp & lim (Partial_Sums (alternating_series a)) = Sum (alternating_series a) )
by A37, SEQ_2:def 7, SERIES_1:def 3;
hence
( (Partial_Sums (alternating_series a)) . (2 * n) >= Sum (alternating_series a) & Sum (alternating_series a) >= (Partial_Sums (alternating_series a)) . ((2 * n) + 1) )
by A46, A11, A12, VALUED_1:def 16, A36, A30, A31, A22, SEQ_2:def 3, A21, SEQ_4:37, SEQ_4:38; verum