let s, s1 be Real_Sequence; :: thesis: ( s is non-increasing & ( for n being Element of 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 Element of 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: now

let n be Element of 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

assume A4: s is summable ; :: thesis: s1 is summable
defpred S₁[ Element of NAT ] means (Partial_Sums s1) . $1 <= 2 * ((Partial_Sums s) . (2 to_power $1));
A5: S₁[ 0 ]

proof

A6: 2 to_power 0 = 0 + 1 by POWER:29;
A7: (Partial_Sums s1) . 0 = s1 . 0 by Def1
.= 1 * (s . 1) by A2, A6
.= s . 1 ;
A8: 2 * ((Partial_Sums s) . (2 to_power 0 )) = 2 * (((Partial_Sums s) . 0 ) + (s . 1)) by A6, Def1
.= 2 * ((s . 0 ) + (s . 1)) by Def1
.= (2 * (s . 0 )) + (2 * (s . 1)) ;
s . 1 >= 0 by A2;
then A9: (s . 1) + (s . 1) >= (s . 1) + 0 by XREAL_1:9;
s . 0 >= 0 by A2;
then (s . 0 ) + (s . 0 ) >= 0 + 0 ;
hence S₁[ 0 ] by A7, A8, A9, XREAL_1:9; :: thesis: verum

end;

A10: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
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:8;
then A11: (Partial_Sums s1) . (n + 1) <= (2 * ((Partial_Sums s) . (2 to_power n))) + (s1 . (n + 1)) by Def1;
deffunc H₁( Element of 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
A12: for m being Element of NAT holds a . m = H₁(m) from SEQ_1:sch 1();
defpred S₂[ Element of NAT ] means ( $1 > 2 to_power n or $1 * (s . (2 to_power (n + 1))) <= a . $1 );
A13: S₂[ 0 ]

proof

a . 0 = ((Partial_Sums s) . ((2 to_power n) + 0 )) - ((Partial_Sums s) . (2 to_power n)) by A12
.= 0 ;
hence S₂[ 0 ] ; :: thesis: verum

end;

A14: for m being Element of NAT st S₂[m] holds
S₂[m + 1]

proof

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

now

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

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

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

end;

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

now

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:9;
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) by POWER:30;
then ((2 to_power n) + m) + 1 <= 2 to_power (n + 1) by POWER:32;
then s . (((2 to_power n) + m) + 1) >= s . (2 to_power (n + 1)) by A1, SEQM_3:14;
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 A16, XREAL_1:9;
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 A12;
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 A12; :: 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;

for m being Element of NAT holds S₂[m] from NAT_1:sch 1(A13, A14);
then 2 * ((2 to_power n) * (s . (2 to_power (n + 1)))) <= 2 * (a . (2 to_power n)) by XREAL_1:66;
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)) by POWER:30;
then (2 to_power (n + 1)) * (s . (2 to_power (n + 1))) <= 2 * (a . (2 to_power n)) by POWER:32;
then s1 . (n + 1) <= 2 * (a . (2 to_power n)) by A2;
then A17: s1 . (n + 1) <= 2 * (((Partial_Sums s) . ((2 to_power n) + (2 to_power n))) - ((Partial_Sums s) . (2 to_power n))) by A12;
A18: (2 to_power n) + (2 to_power n) = 2 * (2 to_power n)
.= (2 to_power 1) * (2 to_power n) by POWER:30
.= 2 to_power (n + 1) by POWER:32 ;
(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 A17, XREAL_1:9;
hence S₁[n + 1] by A11, A18, XXREAL_0:2; :: thesis: verum

end;

A19: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A5, A10);
Partial_Sums s is bounded_above by A2, A4, Th20;
then consider r being real number such that
A20: for n being Element of NAT holds (Partial_Sums s) . n < r by SEQ_2:def 3;

now

let n be Element of NAT ; :: thesis: (Partial_Sums s1) . n < 2 * r
A21: 2 * ((Partial_Sums s) . (2 to_power n)) < 2 * r by A20, XREAL_1:70;
(Partial_Sums s1) . n <= 2 * ((Partial_Sums s) . (2 to_power n)) by A19;
hence (Partial_Sums s1) . n < 2 * r by A21, XXREAL_0:2; :: thesis: verum

end;

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

end;

assume A22: s1 is summable ; :: thesis: s is summable
defpred S₁[ Element of NAT ] means (Partial_Sums s) . (2 to_power ($1 + 1)) <= (((Partial_Sums s1) . $1) + (s . 0 )) + (s . 2);
A23: S₁[ 0 ]

proof

A24: (Partial_Sums s) . (2 to_power (0 + 1)) = (Partial_Sums s) . (1 + 1) by POWER:30
.= ((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 ;
A25: 2 to_power 0 = 1 by POWER:29;
(((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 A25 ;
hence S₁[ 0 ] by A24; :: thesis: verum

end;

A26: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
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:9;
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;
defpred S₂[ Element of 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)));
A28: S₂[ 0 ] ;
A29: for m being Element of NAT st S₂[m] holds
S₂[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₂[m] implies S₂[m + 1] )
assume A30: ((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]
(2 to_power (n + 1)) + (m + 1) >= 2 to_power (n + 1) by NAT_1:11;
then s . ((2 to_power (n + 1)) + (m + 1)) <= s . (2 to_power (n + 1)) by A1, SEQM_3:14;
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 A30, XREAL_1:9;
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;

for m being Element of NAT holds S₂[m] from NAT_1:sch 1(A28, A29);
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 A31: ((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;
(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)) by POWER:30
.= 2 to_power ((n + 1) + 1) by POWER:32 ;
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 A31, XREAL_1:9;
hence S₁[n + 1] by A27, XXREAL_0:2; :: thesis: verum

end;

A32: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A23, A26);
A33: Partial_Sums s is non-decreasing by A2, Th19;
Partial_Sums s1 is bounded_above by A3, A22, Th20;
then consider r being real number such that
A34: for n being Element of NAT holds (Partial_Sums s1) . n < r by SEQ_2:def 3;

now

let n be Element of NAT ; :: thesis: (Partial_Sums s) . n < r + ((s . 0 ) + (s . 2))
A35: (1 + 1) to_power n >= 1 + (n * 1) by POWER:56;
1 + n >= n by NAT_1:11;
then 2 to_power n >= n by A35, XXREAL_0:2;
then (2 to_power n) + (2 to_power n) >= n + n by XREAL_1:9;
then 2 * (2 to_power n) >= n + n ;
then (2 to_power 1) * (2 to_power n) >= n + n by POWER:30;
then A36: 2 to_power (n + 1) >= n + n by POWER:32;
n + n >= n by NAT_1:11;
then 2 to_power (n + 1) >= n by A36, XXREAL_0:2;
then A37: (Partial_Sums s) . (2 to_power (n + 1)) >= (Partial_Sums s) . n by A33, SEQM_3:12;
(Partial_Sums s) . (2 to_power (n + 1)) <= (((Partial_Sums s1) . n) + (s . 0 )) + (s . 2) by A32;
then A38: (Partial_Sums s) . n <= (((Partial_Sums s1) . n) + (s . 0 )) + (s . 2) by A37, XXREAL_0:2;
(Partial_Sums s1) . n < r by A34;
then ((Partial_Sums s1) . n) + ((s . 0 ) + (s . 2)) < r + ((s . 0 ) + (s . 2)) by XREAL_1:8;
hence (Partial_Sums s) . n < r + ((s . 0 ) + (s . 2)) by A38, XXREAL_0:2; :: thesis: verum

end;

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