let s, s1 be Real_Sequence; :: thesis: ( s is non-increasing & ( for n being Nat holds
( s . n >= 0 & s1 . n = (2 to_power n) * (s . (2 to_power n)) ) ) implies ( s is summable iff s1 is summable ) )
assume that
A1: s is non-increasing and
A2: for n being Nat holds
( s . n >= 0 & s1 . n = (2 to_power n) * (s . (2 to_power n)) ) ; :: thesis: ( s is summable iff s1 is summable )
A3: (Partial_Sums s) . (2 to_power (0 + 1)) = (Partial_Sums s) . (1 + 1)
.= ((Partial_Sums s) . (0 + 1)) + (s . 2) by Def1
.= (((Partial_Sums s) . 0) + (s . 1)) + (s . 2) by Def1
.= ((s . 0) + (s . 1)) + (s . 2) by Def1 ;

A4: now :: thesis: for n being Nat holds s1 . n >= 0

let n be Nat; :: thesis: s1 . n >= 0
s . (2 to_power n) >= 0 by A2;
then (2 to_power n) * (s . (2 to_power n)) >= 0 ;
hence s1 . n >= 0 by A2; :: thesis: verum

end;

thus ( s is summable implies s1 is summable ) :: thesis: ( s1 is summable implies s is summable )

proof

defpred S₁[ Nat] means (Partial_Sums s1) . $1 <= 2 * ((Partial_Sums s) . (2 to_power $1));
A5: s . 0 >= 0 by A2;
A6: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
deffunc H₁( Nat) -> Element of REAL = ((Partial_Sums s) . ((2 to_power n) + $1)) - ((Partial_Sums s) . (2 to_power n));
consider a being Real_Sequence such that
A7: for m being Nat holds a . m = H₁(m) from SEQ_1:sch 1();
defpred S₂[ Nat] means ( $1 > 2 to_power n or $1 * (s . (2 to_power (n + 1))) <= a . $1 );
A8: for m being Nat st S₂[m] holds
S₂[m + 1]

proof

let m be Nat; :: thesis: ( S₂[m] implies S₂[m + 1] )
assume A9: ( m > 2 to_power n or m * (s . (2 to_power (n + 1))) <= a . m ) ; :: thesis: S₂[m + 1]

now :: thesis: S₂[m + 1]

per cases ( m > 2 to_power n or m * (s . (2 to_power (n + 1))) <= a . m ) by A9;

suppose m > 2 to_power n ; :: thesis: S₂[m + 1]

hence S₂[m + 1] by NAT_1:13; :: thesis: verum

end;

suppose A10: m * (s . (2 to_power (n + 1))) <= a . m ; :: thesis: S₂[m + 1]

now :: thesis: S₂[m + 1]

per cases ( m < 2 to_power n or m >= 2 to_power n ) ;

suppose m < 2 to_power n ; :: thesis: S₂[m + 1]

then m + 1 <= 2 to_power n by NAT_1:13;
then (2 to_power n) + (m + 1) <= (2 to_power n) + (2 to_power n) by XREAL_1:7;
then ((2 to_power n) + m) + 1 <= 2 * (2 to_power n) ;
then ((2 to_power n) + m) + 1 <= (2 to_power 1) * (2 to_power n) ;
then ((2 to_power n) + m) + 1 <= 2 to_power (n + 1) by POWER:27;
then s . (((2 to_power n) + m) + 1) >= s . (2 to_power (n + 1)) by A1, SEQM_3:8;
then (m * (s . (2 to_power (n + 1)))) + (1 * (s . (2 to_power (n + 1)))) <= (a . m) + (s . (((2 to_power n) + m) + 1)) by A10, XREAL_1:7;
then (m + 1) * (s . (2 to_power (n + 1))) <= (((Partial_Sums s) . ((2 to_power n) + m)) - ((Partial_Sums s) . (2 to_power n))) + (s . (((2 to_power n) + m) + 1)) by A7;
then (m + 1) * (s . (2 to_power (n + 1))) <= (((Partial_Sums s) . ((2 to_power n) + m)) + (s . (((2 to_power n) + m) + 1))) - ((Partial_Sums s) . (2 to_power n)) ;
then (m + 1) * (s . (2 to_power (n + 1))) <= ((Partial_Sums s) . ((2 to_power n) + (m + 1))) - ((Partial_Sums s) . (2 to_power n)) by Def1;
hence S₂[m + 1] by A7; :: thesis: verum

end;

suppose m >= 2 to_power n ; :: thesis: S₂[m + 1]

hence S₂[m + 1] by NAT_1:13; :: thesis: verum

end;

end;

end;

hence S₂[m + 1] ; :: thesis: verum

end;

end;

end;

hence S₂[m + 1] ; :: thesis: verum

end;

a . 0 = ((Partial_Sums s) . ((2 to_power n) + 0)) - ((Partial_Sums s) . (2 to_power n)) by A7
.= 0 ;
then A11: S₂[ 0 ] ;
for m being Nat holds S₂[m] from NAT_1:sch 2(A11, A8);
then 2 * ((2 to_power n) * (s . (2 to_power (n + 1)))) <= 2 * (a . (2 to_power n)) by XREAL_1:64;
then (2 * (2 to_power n)) * (s . (2 to_power (n + 1))) <= 2 * (a . (2 to_power n)) ;
then ((2 to_power 1) * (2 to_power n)) * (s . (2 to_power (n + 1))) <= 2 * (a . (2 to_power n)) ;
then (2 to_power (n + 1)) * (s . (2 to_power (n + 1))) <= 2 * (a . (2 to_power n)) by POWER:27;
then s1 . (n + 1) <= 2 * (a . (2 to_power n)) by A2;
then s1 . (n + 1) <= 2 * (((Partial_Sums s) . ((2 to_power n) + (2 to_power n))) - ((Partial_Sums s) . (2 to_power n))) by A7;
then A12: (2 * ((Partial_Sums s) . (2 to_power n))) + (s1 . (n + 1)) <= (2 * ((Partial_Sums s) . (2 to_power n))) + (2 * (((Partial_Sums s) . ((2 to_power n) + (2 to_power n))) - ((Partial_Sums s) . (2 to_power n)))) by XREAL_1:7;
assume (Partial_Sums s1) . n <= 2 * ((Partial_Sums s) . (2 to_power n)) ; :: thesis: S₁[n + 1]
then ((Partial_Sums s1) . n) + (s1 . (n + 1)) <= (2 * ((Partial_Sums s) . (2 to_power n))) + (s1 . (n + 1)) by XREAL_1:6;
then A13: (Partial_Sums s1) . (n + 1) <= (2 * ((Partial_Sums s) . (2 to_power n))) + (s1 . (n + 1)) by Def1;
(2 to_power n) + (2 to_power n) = 2 * (2 to_power n)
.= (2 to_power 1) * (2 to_power n)
.= 2 to_power (n + 1) by POWER:27 ;
hence S₁[n + 1] by A13, A12, XXREAL_0:2; :: thesis: verum

end;

A14: 2 to_power 0 = 0 + 1 by POWER:24;
then A15: 2 * ((Partial_Sums s) . (2 to_power 0)) = 2 * (((Partial_Sums s) . 0) + (s . 1)) by Def1
.= 2 * ((s . 0) + (s . 1)) by Def1
.= (2 * (s . 0)) + (2 * (s . 1)) ;
assume s is summable ; :: thesis: s1 is summable
then Partial_Sums s is bounded_above ;
then consider r being Real such that
A16: for n being Nat holds (Partial_Sums s) . n < r by SEQ_2:def 3;
s . 1 >= 0 by A2;
then A17: (s . 1) + (s . 1) >= (s . 1) + 0 by XREAL_1:7;
(Partial_Sums s1) . 0 = s1 . 0 by Def1
.= 1 * (s . 1) by A2, A14
.= s . 1 ;
then A18: S₁[ 0 ] by A15, A17, A5, XREAL_1:7;
A19: for n being Nat holds S₁[n] from NAT_1:sch 2(A18, A6);

now :: thesis: for n being Nat holds (Partial_Sums s1) . n < 2 * r

let n be Nat; :: thesis: (Partial_Sums s1) . n < 2 * r
( 2 * ((Partial_Sums s) . (2 to_power n)) < 2 * r & (Partial_Sums s1) . n <= 2 * ((Partial_Sums s) . (2 to_power n)) ) by A19, A16, XREAL_1:68;
hence (Partial_Sums s1) . n < 2 * r by XXREAL_0:2; :: thesis: verum

end;

then Partial_Sums s1 is bounded_above by SEQ_2:def 3;
hence s1 is summable by A4, Th17; :: thesis: verum

end;

assume s1 is summable ; :: thesis: s is summable
then Partial_Sums s1 is bounded_above ;
then consider r being Real such that
A20: for n being Nat holds (Partial_Sums s1) . n < r by SEQ_2:def 3;
A21: 2 to_power 0 = 1 by POWER:24;
defpred S₁[ Nat] means (Partial_Sums s) . (2 to_power ($1 + 1)) <= (((Partial_Sums s1) . $1) + (s . 0)) + (s . 2);
A22: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
defpred S₂[ Nat] means ((Partial_Sums s) . ((2 to_power (n + 1)) + $1)) - ((Partial_Sums s) . (2 to_power (n + 1))) <= $1 * (s . (2 to_power (n + 1)));
A23: for m being Nat st S₂[m] holds
S₂[m + 1]

proof

let m be Nat; :: thesis: ( S₂[m] implies S₂[m + 1] )
(2 to_power (n + 1)) + (m + 1) >= 2 to_power (n + 1) by NAT_1:11;
then A24: s . ((2 to_power (n + 1)) + (m + 1)) <= s . (2 to_power (n + 1)) by A1, SEQM_3:8;
assume ((Partial_Sums s) . ((2 to_power (n + 1)) + m)) - ((Partial_Sums s) . (2 to_power (n + 1))) <= m * (s . (2 to_power (n + 1))) ; :: thesis: S₂[m + 1]
then (((Partial_Sums s) . ((2 to_power (n + 1)) + m)) - ((Partial_Sums s) . (2 to_power (n + 1)))) + (s . (((2 to_power (n + 1)) + m) + 1)) <= (m * (s . (2 to_power (n + 1)))) + (s . (2 to_power (n + 1))) by A24, XREAL_1:7;
then (((Partial_Sums s) . ((2 to_power (n + 1)) + m)) + (s . (((2 to_power (n + 1)) + m) + 1))) - ((Partial_Sums s) . (2 to_power (n + 1))) <= (m * (s . (2 to_power (n + 1)))) + (s . (2 to_power (n + 1))) ;
hence S₂[m + 1] by Def1; :: thesis: verum

end;

A25: S₂[ 0 ] ;
for m being Nat holds S₂[m] from NAT_1:sch 2(A25, A23);
then ((Partial_Sums s) . ((2 to_power (n + 1)) + (2 to_power (n + 1)))) - ((Partial_Sums s) . (2 to_power (n + 1))) <= (2 to_power (n + 1)) * (s . (2 to_power (n + 1))) ;
then A26: ((Partial_Sums s) . ((2 to_power (n + 1)) + (2 to_power (n + 1)))) - ((Partial_Sums s) . (2 to_power (n + 1))) <= s1 . (n + 1) by A2;
assume (Partial_Sums s) . (2 to_power (n + 1)) <= (((Partial_Sums s1) . n) + (s . 0)) + (s . 2) ; :: thesis: S₁[n + 1]
then ((Partial_Sums s) . (2 to_power (n + 1))) + (s1 . (n + 1)) <= (s1 . (n + 1)) + ((((Partial_Sums s1) . n) + (s . 0)) + (s . 2)) by XREAL_1:7;
then ((Partial_Sums s) . (2 to_power (n + 1))) + (s1 . (n + 1)) <= ((((Partial_Sums s1) . n) + (s1 . (n + 1))) + (s . 0)) + (s . 2) ;
then A27: ((Partial_Sums s) . (2 to_power (n + 1))) + (s1 . (n + 1)) <= (((Partial_Sums s1) . (n + 1)) + (s . 0)) + (s . 2) by Def1;
(2 to_power (n + 1)) + (2 to_power (n + 1)) = 2 * (2 to_power (n + 1))
.= (2 to_power 1) * (2 to_power (n + 1))
.= 2 to_power ((n + 1) + 1) by POWER:27 ;
then (((Partial_Sums s) . (2 to_power ((n + 1) + 1))) - ((Partial_Sums s) . (2 to_power (n + 1)))) + ((Partial_Sums s) . (2 to_power (n + 1))) <= ((Partial_Sums s) . (2 to_power (n + 1))) + (s1 . (n + 1)) by A26, XREAL_1:7;
hence S₁[n + 1] by A27, XXREAL_0:2; :: thesis: verum

end;

(((Partial_Sums s1) . 0) + (s . 0)) + (s . 2) = ((s1 . 0) + (s . 0)) + (s . 2) by Def1
.= (((2 to_power 0) * (s . (2 to_power 0))) + (s . 0)) + (s . 2) by A2
.= ((s . 0) + (s . 1)) + (s . 2) by A21 ;
then A28: S₁[ 0 ] by A3;
A29: for n being Nat holds S₁[n] from NAT_1:sch 2(A28, A22);
A30: Partial_Sums s is non-decreasing by A2, Th16;

now :: thesis: for n being Nat holds (Partial_Sums s) . n < r + ((s . 0) + (s . 2))

let n be Nat; :: thesis: (Partial_Sums s) . n < r + ((s . 0) + (s . 2))
(Partial_Sums s1) . n < r by A20;
then A31: ((Partial_Sums s1) . n) + ((s . 0) + (s . 2)) < r + ((s . 0) + (s . 2)) by XREAL_1:6;
( (1 + 1) to_power n >= 1 + (n * 1) & 1 + n >= n ) by NAT_1:11, POWER:49;
then 2 to_power n >= n by XXREAL_0:2;
then (2 to_power n) + (2 to_power n) >= n + n by XREAL_1:7;
then 2 * (2 to_power n) >= n + n ;
then (2 to_power 1) * (2 to_power n) >= n + n ;
then A32: 2 to_power (n + 1) >= n + n by POWER:27;
n + n >= n by NAT_1:11;
then 2 to_power (n + 1) >= n by A32, XXREAL_0:2;
then A33: (Partial_Sums s) . (2 to_power (n + 1)) >= (Partial_Sums s) . n by A30, SEQM_3:6;
(Partial_Sums s) . (2 to_power (n + 1)) <= (((Partial_Sums s1) . n) + (s . 0)) + (s . 2) by A29;
then (Partial_Sums s) . n <= (((Partial_Sums s1) . n) + (s . 0)) + (s . 2) by A33, XXREAL_0:2;
hence (Partial_Sums s) . n < r + ((s . 0) + (s . 2)) by A31, XXREAL_0:2; :: thesis: verum

end;

then Partial_Sums s is bounded_above by SEQ_2:def 3;
hence s is summable by A2, Th17; :: thesis: verum