let p be real number ; :: thesis: for s being Real_Sequence st p > 1 & ( for n being Element of NAT st n >= 1 holds
s . n = 1 / (n to_power p) ) holds
s is summable
let s be Real_Sequence; :: thesis: ( p > 1 & ( for n being Element of NAT st n >= 1 holds
s . n = 1 / (n to_power p) ) implies s is summable )
assume that
A1: p > 1 and
A2: for n being Element of NAT st n >= 1 holds
s . n = 1 / (n to_power p) ; :: thesis: s is summable
defpred S₁[ Element of NAT , real number ] means ( ( $1 = 0 & $2 = 1 ) or ( $1 >= 1 & $2 = 1 / ($1 to_power p) ) );
A3: for n being Element of NAT ex r being Real st S₁[n,r]

proof

let n be Element of NAT ; :: thesis: ex r being Real st S₁[n,r]
( n = 0 or n >= 1 )

proof

assume A4: ( n <> 0 & n < 1 ) ; :: thesis: contradiction
then n > 0 ;
then n >= 0 + 1 by NAT_1:13;
hence contradiction by A4; :: thesis: verum

end;

hence ex r being Real st S₁[n,r] ; :: thesis: verum

end;

consider s1 being Real_Sequence such that
A5: for n being Element of NAT holds S₁[n,s1 . n] from FUNCT_2:sch 3(A3);
A6: s1 . 0 = 1 by A5;

now

let n be Element of NAT ; :: thesis: s1 . (n + 1) <= s1 . n

now

per cases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;

suppose A7: n = 0 ; :: thesis: s1 . (n + 1) <= s1 . n

A8: s1 . (n + 1) = 1 / ((n + 1) to_power p) by A5;
(n + 1) #R p >= 1 by A1, A7, PREPOWER:99;
then (n + 1) to_power p >= 1 by POWER:def 2;
hence s1 . (n + 1) <= s1 . n by A6, A7, A8, XREAL_1:213; :: thesis: verum

end;

suppose ex m being Nat st n = m + 1 ; :: thesis: s1 . (n + 1) <= s1 . n

then consider m being Nat such that
A9: n = m + 1 ;
A10: n to_power p > 0 by A9, POWER:39;
A11: n / (n + 1) > 0 by A9, XREAL_1:141;
A12: (s1 . (n + 1)) / (s1 . n) = (1 / ((n + 1) to_power p)) / (s1 . n) by A5
.= (1 / ((n + 1) to_power p)) / (1 / (n to_power p)) by A5, A9
.= (1 / ((n + 1) to_power p)) * (n to_power p)
.= (n to_power p) / ((n + 1) to_power p)
.= (n / (n + 1)) to_power p by A9, POWER:36
.= (n / (n + 1)) #R p by A11, POWER:def 2 ;
1 / (n to_power p) > 0 by A10;
then A13: s1 . n > 0 by A5;
n <= n + 1 by NAT_1:11;
then n / (n + 1) <= 1 by XREAL_1:185;
then (s1 . (n + 1)) / (s1 . n) <= (n / (n + 1)) #R 0 by A1, A11, A12, PREPOWER:98;
then (s1 . (n + 1)) / (s1 . n) <= 1 by A9, PREPOWER:85, XREAL_1:141;
hence s1 . (n + 1) <= s1 . n by A13, XREAL_1:189; :: thesis: verum

end;

end;

end;

hence s1 . (n + 1) <= s1 . n ; :: thesis: verum

end;

then A14: s1 is non-increasing by SEQM_3:def 14;
deffunc H₁( Element of NAT ) -> Element of REAL = (2 to_power $1) * (s1 . (2 to_power $1));
consider s2 being Real_Sequence such that
A15: for n being Element of NAT holds s2 . n = H₁(n) from SEQ_1:sch 1();

A16: now

let n be Element of NAT ; :: thesis: ( s1 . n >= 0 & s2 . n = (2 to_power n) * (s1 . (2 to_power n)) )

now

per cases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;

suppose n = 0 ; :: thesis: s1 . n >= 0

hence s1 . n >= 0 by A5; :: thesis: verum

end;

suppose ex m being Nat st n = m + 1 ; :: thesis: s1 . n >= 0

then consider m being Nat such that
A17: n = m + 1 ;
n to_power p > 0 by A17, POWER:39;
then 1 / (n to_power p) >= 0 ;
hence s1 . n >= 0 by A5; :: thesis: verum

end;

end;

end;

hence ( s1 . n >= 0 & s2 . n = (2 to_power n) * (s1 . (2 to_power n)) ) by A15; :: thesis: verum

end;

deffunc H₂( Element of NAT ) -> Element of REAL = $1 -root (s2 . $1);
consider s3 being Real_Sequence such that
A18: for n being Element of NAT holds s3 . n = H₂(n) from SEQ_1:sch 1();

A19: now

let n be Element of NAT ; :: thesis: ( s2 . n = 2 to_power ((1 - p) * n) & s2 . n >= 0 & s3 . n = n -root ((2 to_power (1 - p)) to_power n) )
A20: 2 to_power n > 0 by POWER:39;
thus A21: s2 . n = (2 to_power n) * (s1 . (2 to_power n)) by A15
.= (2 to_power n) * (1 / ((2 to_power n) to_power p)) by A5, A20
.= (2 to_power n) * (1 / (2 to_power (n * p))) by POWER:38
.= (2 to_power n) * (2 to_power (- (n * p))) by POWER:33
.= 2 to_power (n + (- (n * p))) by POWER:32
.= 2 to_power ((1 - p) * n) ; :: thesis: ( s2 . n >= 0 & s3 . n = n -root ((2 to_power (1 - p)) to_power n) )
hence s2 . n >= 0 by POWER:39; :: thesis: s3 . n = n -root ((2 to_power (1 - p)) to_power n)
s2 . n = (2 to_power (1 - p)) to_power n by A21, POWER:38;
hence s3 . n = n -root ((2 to_power (1 - p)) to_power n) by A18; :: thesis: verum

end;

A22: now

let n be Nat; :: thesis: (s3 ^\ 1) . n = 2 to_power (1 - p)
A23: n + 1 >= 0 + 1 by XREAL_1:8;
A24: ( 2 to_power (1 - p) <> 0 & 2 to_power (1 - p) >= 0 ) by POWER:39;
thus (s3 ^\ 1) . n = s3 . (n + 1) by NAT_1:def 3
.= (n + 1) -root ((2 to_power (1 - p)) to_power (n + 1)) by A19
.= 2 to_power (1 - p) by A23, A24, POWER:5 ; :: thesis: verum

end;

then A25: s3 ^\ 1 is V8() by VALUED_0:def 18;
then A26: s3 is convergent by SEQ_4:35;
lim (s3 ^\ 1) = (s3 ^\ 1) . 0 by A25, SEQ_4:41
.= 2 to_power (1 - p) by A22 ;
then A27: lim s3 = 2 to_power (1 - p) by A25, SEQ_4:36;
( 1 - p < 0 & 2 > 1 ) by A1, XREAL_1:51;
then lim s3 < 1 by A27, POWER:41;
then s2 is summable by A18, A19, A26, Th32;
then s1 is summable by A14, A16, Th35;
then A28: s1 ^\ 1 is summable by Th15;

A29: now

let n be Element of NAT ; :: thesis: (s ^\ 1) . n >= 0
A30: n + 1 >= 0 + 1 by XREAL_1:8;
A31: (s ^\ 1) . n = s . (n + 1) by NAT_1:def 3
.= 1 / ((n + 1) to_power p) by A2, A30
.= s1 . (n + 1) by A5
.= (s1 ^\ 1) . n by NAT_1:def 3 ;
s1 . (n + 1) >= 0 by A16;
hence (s ^\ 1) . n >= 0 by A31, NAT_1:def 3; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: ( n >= 0 implies (s1 ^\ 1) . n >= (s ^\ 1) . n )
assume n >= 0 ; :: thesis: (s1 ^\ 1) . n >= (s ^\ 1) . n
A32: n + 1 >= 0 + 1 by XREAL_1:8;
(s ^\ 1) . n = s . (n + 1) by NAT_1:def 3
.= 1 / ((n + 1) to_power p) by A2, A32
.= s1 . (n + 1) by A5
.= (s1 ^\ 1) . n by NAT_1:def 3 ;
hence (s1 ^\ 1) . n >= (s ^\ 1) . n ; :: thesis: verum

end;

then s ^\ 1 is summable by A28, A29, Th22;
hence s is summable by Th16; :: thesis: verum