let a be Real_Sequence; :: thesis: ( 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 ) ; :: thesis: ( 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 S₁[ Nat, object ] means $2 = (Partial_Sums (alternating_series a)) . (2 * $1);
defpred S₂[ 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 S₁[x,y] ;
A3: for x being Element of NAT ex y being Element of REAL st S₂[x,y] ;
consider Sp being Function of NAT,REAL such that
A4: for x being Element of NAT holds S₁[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 S₂[x,Sn . x] from FUNCT_2:sch 3(A3);
A6: for n being Nat holds Sn . n <= Sn . (n + 1)

proof

let n be Nat; :: thesis: Sn . n <= Sn . (n + 1)
set n1 = n + 1;
A7: ( n + 1 in NAT & n in NAT ) by ORDINAL1:def 12;
A8: Sn . (n + 1) = (Partial_Sums (alternating_series a)) . ((2 * (n + 1)) + 1) by A5
.= ((Partial_Sums (alternating_series a)) . (((2 * n) + 1) + 1)) + ((alternating_series a) . ((2 * (n + 1)) + 1)) by SERIES_1:def 1
.= (((Partial_Sums (alternating_series a)) . ((2 * n) + 1)) + ((alternating_series a) . (2 * (n + 1)))) + ((alternating_series a) . ((2 * (n + 1)) + 1)) by SERIES_1:def 1
.= ((Partial_Sums (alternating_series a)) . ((2 * n) + 1)) + (((alternating_series a) . (2 * (n + 1))) + ((alternating_series a) . ((2 * (n + 1)) + 1))) ;
A9: Sn . n = (Partial_Sums (alternating_series a)) . ((2 * n) + 1) by A7, A5;
A10: (a . (2 * (n + 1))) - (a . ((2 * (n + 1)) + 1)) >= 0 by XREAL_1:48, A1, VALUED_1:def 16;
( (- 1) |^ (2 * (n + 1)) = 1 & (- 1) |^ ((2 * (n + 1)) + 1) = - 1 ) ;
then ( (alternating_series a) . (2 * (n + 1)) = 1 * (a . (2 * (n + 1))) & (alternating_series a) . ((2 * (n + 1)) + 1) = (- 1) * (a . ((2 * (n + 1)) + 1)) ) by Def1;
hence Sn . n <= Sn . (n + 1) by A10, A9, A8, XREAL_1:31; :: thesis: verum

end;

then A11: Sn is non-decreasing by VALUED_1:def 15;
A12: for n being Nat holds Sp . n >= Sp . (n + 1)

proof

let n be Nat; :: thesis: Sp . n >= Sp . (n + 1)
set n1 = n + 1;
A13: ( n + 1 in NAT & n in NAT & 2 * (n + 1) = ((2 * n) + 1) + 1 ) by ORDINAL1:def 12;
then A14: Sp . (n + 1) = (Partial_Sums (alternating_series a)) . (((2 * n) + 1) + 1) by A4
.= ((Partial_Sums (alternating_series a)) . ((2 * n) + 1)) + ((alternating_series a) . (((2 * n) + 1) + 1)) by SERIES_1:def 1
.= (((Partial_Sums (alternating_series a)) . (2 * n)) + ((alternating_series a) . ((2 * n) + 1))) + ((alternating_series a) . (((2 * n) + 1) + 1)) by SERIES_1:def 1
.= ((Partial_Sums (alternating_series a)) . (2 * n)) + (((alternating_series a) . ((2 * n) + 1)) + ((alternating_series a) . (2 * (n + 1)))) ;
A15: Sp . n = (Partial_Sums (alternating_series a)) . (2 * n) by A13, A4;
a . ((2 * n) + 1) >= a . (((2 * n) + 1) + 1) by A1, VALUED_1:def 16;
then A16: (a . (2 * (n + 1))) - (a . ((2 * n) + 1)) <= 0 by XREAL_1:47;
( (- 1) |^ (2 * (n + 1)) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 ) ;
then ( (alternating_series a) . (2 * (n + 1)) = 1 * (a . (2 * (n + 1))) & (alternating_series a) . ((2 * n) + 1) = (- 1) * (a . ((2 * n) + 1)) ) by Def1;
hence Sp . n >= Sp . (n + 1) by A15, A14, XREAL_1:32, A16; :: thesis: verum

end;

then A17: Sp is non-increasing by VALUED_1:def 16;
A18: for n being Nat holds Sp . n >= Sn . n

proof

let n be Nat; :: thesis: Sp . n >= Sn . n
n in NAT by ORDINAL1:def 12;
then ( Sp . n = (Partial_Sums (alternating_series a)) . (2 * n) & Sn . n = (Partial_Sums (alternating_series a)) . ((2 * n) + 1) ) by A4, A5;
then A19: Sn . n = (Sp . n) + ((alternating_series a) . ((2 * n) + 1)) by SERIES_1:def 1;
dom a = NAT by FUNCT_2:def 1;
then a . ((2 * n) + 1) in rng a by FUNCT_1:def 3;
then A20: a . ((2 * n) + 1) >= 0 by A1, PARTFUN3:def 4;
(- 1) |^ ((2 * n) + 1) = - 1 ;
then (alternating_series a) . ((2 * n) + 1) = (- 1) * (a . ((2 * n) + 1)) by Def1;
hence Sp . n >= Sn . n by A19, XREAL_1:32, A20; :: thesis: verum

end;

for n being Nat holds Sp . n > (Sn . 0) - 1

proof

let n be Nat; :: thesis: Sp . n > (Sn . 0) - 1
( Sp . n >= Sn . n & Sn . n >= Sn . 0 ) by A18, A6, VALUED_1:def 15, SEQM_3:6;
then ( Sp . n >= Sn . 0 & Sn . 0 > (Sn . 0) - 1 ) by XXREAL_0:2, XREAL_1:44;
hence Sp . n > (Sn . 0) - 1 by XXREAL_0:2; :: thesis: verum

end;

then A21: Sp is bounded_below by SEQ_2:def 4;
A22: for n being Nat holds Sn . n < (Sp . 0) + 1

proof

let n be Nat; :: thesis: Sn . n < (Sp . 0) + 1
( Sn . n <= Sp . n & Sp . n <= Sp . 0 ) by A18, A12, VALUED_1:def 16, SEQM_3:8;
then ( Sn . n <= Sp . 0 & Sp . 0 < (Sp . 0) + 1 ) by XXREAL_0:2, XREAL_1:29;
hence Sn . n < (Sp . 0) + 1 by XXREAL_0:2; :: thesis: verum

end;

then A23: Sn is bounded_above by SEQ_2:def 3;
deffunc H₁( Nat) -> Element of NAT = (2 * $1) + 1;
A24: for x being Element of NAT holds H₁(x) in NAT ;
consider Double being Function of NAT,NAT such that
A25: for x being Element of NAT holds Double . x = H₁(x) from FUNCT_2:sch 8(A24);
reconsider Double1 = Double as ManySortedSet of NAT ;
for n being Nat holds Double . n < Double . (n + 1)

proof

let n be Nat; :: thesis: Double . n < Double . (n + 1)
set n1 = n + 1;
( n in NAT & n + 1 in NAT ) by ORDINAL1:def 12;
then A26: ( Double . n = H₁(n) & Double . (n + 1) = H₁(n + 1) ) by A25;
n < n + 1 by NAT_1:13;
then 2 * n < 2 * (n + 1) by XREAL_1:97;
hence Double . n < Double . (n + 1) by A26, XREAL_1:8; :: thesis: verum

end;

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

proof

let x be object ; :: thesis: ( x in NAT implies aD . x = (Sp - Sn) . x )
assume A32: x in NAT ; :: thesis: aD . x = (Sp - Sn) . x
reconsider n = x as Element of NAT by A32;
A33: Double . n = (2 * n) + 1 by A25;
dom (Sp - Sn) = NAT by FUNCT_2:def 1;
then A34: (Sp - Sn) . n = (Sp . n) - (Sn . n) by VALUED_1:13;
( Sp . n = (Partial_Sums (alternating_series a)) . (2 * n) & Sn . n = (Partial_Sums (alternating_series a)) . ((2 * n) + 1) ) by A4, A5;
then A35: Sn . n = (Sp . n) + ((alternating_series a) . ((2 * n) + 1)) by SERIES_1:def 1;
(- 1) |^ ((2 * n) + 1) = - 1 ;
then (alternating_series a) . ((2 * n) + 1) = (- 1) * (a . ((2 * n) + 1)) by Def1;
hence aD . x = (Sp - Sn) . x by A29, A34, A35, FUNCT_1:12, A33; :: thesis: verum

end;

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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: for m being Nat st N <= m holds
|.(((Partial_Sums (alternating_series a)) . m) - (lim Sp)).| < p
let m be Nat; :: thesis: ( N <= m implies |.(((Partial_Sums (alternating_series a)) . m) - (lim Sp)).| < p )
assume A41: N <= m ; :: thesis: |.(((Partial_Sums (alternating_series a)) . m) - (lim Sp)).| < p

per cases ( m is even or m is odd ) ;

suppose m is even ; :: thesis: |.(((Partial_Sums (alternating_series a)) . m) - (lim Sp)).| < p

then consider m2 being Nat such that
A42: m = 2 * m2 by ABIAN:def 2;
2 * n1 <= N by XXREAL_0:25;
then 2 * n1 <= 2 * m2 by A41, A42, XXREAL_0:2;
then n1 <= m2 by XREAL_1:68;
then A43: |.((Sp . m2) - (lim Sp)).| < p by A39;
m2 in NAT by ORDINAL1:def 12;
hence |.(((Partial_Sums (alternating_series a)) . m) - (lim Sp)).| < p by A4, A43, A42; :: thesis: verum

end;

suppose m is odd ; :: thesis: |.(((Partial_Sums (alternating_series a)) . m) - (lim Sp)).| < p

then consider m2 being Nat such that
A44: m = (2 * m2) + 1 by ABIAN:9;
(2 * n2) + 1 <= N by XXREAL_0:25;
then (2 * n2) + 1 <= (2 * m2) + 1 by A41, A44, XXREAL_0:2;
then 2 * n2 <= 2 * m2 by XREAL_1:6;
then n2 <= m2 by XREAL_1:68;
then A45: |.((Sn . m2) - (lim Sp)).| < p by A40;
m2 in NAT by ORDINAL1:def 12;
hence |.(((Partial_Sums (alternating_series a)) . m) - (lim Sp)).| < p by A45, A44, A5; :: thesis: verum

end;

end;

end;

hence alternating_series a is summable by SERIES_1:def 2, SEQ_2:def 6; :: thesis: 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; :: thesis: ( (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; :: thesis: verum