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
not 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 not 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: not s is summable

now

per cases ( p < 0 or p >= 0 ) ;

suppose p < 0 ; :: thesis: not s is summable

then A3: - p >= 0 ;

now

assume ( s is convergent & lim s = 0 ) ; :: thesis: contradiction
then consider m being Element of NAT such that
A4: for n being Element of NAT st n >= m holds
abs ((s . n) - 0 ) < 1 by SEQ_2:def 7;
consider k being Element of NAT such that
A5: k > m by SEQ_4:10;

now

let n be Element of NAT ; :: thesis: not n >= k
assume A6: n >= k ; :: thesis: contradiction
A7: n > 0 by A5, A6;
then A8: n >= 0 + 1 by NAT_1:13;
n >= m by A5, A6, XXREAL_0:2;
then abs ((s . n) - 0 ) < 1 by A4;
then abs (1 / (n to_power p)) < 1 by A2, A8;
then abs (n to_power (- p)) < 1 by A7, POWER:33;
then A9: n to_power (- p) < 1 by ABSVALUE:def 1;
n #R (- p) >= 1 by A3, A8, PREPOWER:99;
hence contradiction by A7, A9, POWER:def 2; :: thesis: verum

end;

hence contradiction ; :: thesis: verum

end;

hence not s is summable by Th7; :: thesis: verum

end;

suppose A10: p >= 0 ; :: thesis: not s is summable

defpred S₁[ Element of NAT , real number ] means ( ( $1 = 0 & $2 = 1 ) or ( $1 >= 1 & $2 = 1 / ($1 to_power p) ) );
A11: 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 A12: ( n <> 0 & n < 1 ) ; :: thesis: contradiction
then n > 0 ;
then n >= 0 + 1 by NAT_1:13;
hence contradiction by A12; :: thesis: verum

end;

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

end;

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

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 A15: n = 0 ; :: thesis: s1 . (n + 1) <= s1 . n

A16: s1 . (n + 1) = 1 / ((n + 1) to_power p) by A13;
(n + 1) #R p >= 1 by A10, A15, PREPOWER:99;
then (n + 1) to_power p >= 1 by POWER:def 2;
hence s1 . (n + 1) <= s1 . n by A14, A15, A16, 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
A17: n = m + 1 ;
A18: n to_power p > 0 by A17, POWER:39;
A19: n / (n + 1) > 0 by A17, XREAL_1:141;
A20: (s1 . (n + 1)) / (s1 . n) = (1 / ((n + 1) to_power p)) / (s1 . n) by A13
.= (1 / ((n + 1) to_power p)) / (1 / (n to_power p)) by A13, A17
.= (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 A17, POWER:36
.= (n / (n + 1)) #R p by A19, POWER:def 2 ;
1 / (n to_power p) > 0 by A18;
then A21: s1 . n > 0 by A13;
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 A10, A19, A20, PREPOWER:98;
then (s1 . (n + 1)) / (s1 . n) <= 1 by A17, PREPOWER:85, XREAL_1:141;
hence s1 . (n + 1) <= s1 . n by A21, XREAL_1:189; :: thesis: verum

end;

end;

end;

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

end;

then A22: 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
A23: for n being Element of NAT holds s2 . n = H₁(n) from SEQ_1:sch 1();

A24: 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 A13; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

now

assume ( s2 is convergent & lim s2 = 0 ) ; :: thesis: contradiction
then consider m being Element of NAT such that
A26: for n being Element of NAT st n >= m holds
abs ((s2 . n) - 0 ) < 1 / 2 by SEQ_2:def 7;

now

let n be Element of NAT ; :: thesis: not n >= m
assume n >= m ; :: thesis: contradiction
then abs ((s2 . n) - 0 ) < 1 / 2 by A26;
then A27: abs ((2 to_power n) * (s1 . (2 to_power n))) < 1 / 2 by A23;
2 to_power n >= 1 by PREPOWER:19;
then abs ((2 to_power n) * (1 / ((2 to_power n) to_power p))) < 1 / 2 by A13, A27;
then abs ((2 to_power n) * (1 / (2 to_power (n * p)))) < 1 / 2 by POWER:38;
then abs ((2 to_power n) * (2 to_power (- (n * p)))) < 1 / 2 by POWER:33;
then abs (2 to_power (n + (- (n * p)))) < 1 / 2 by POWER:32;
then 2 to_power (n - (n * p)) < 1 / 2 by ABSVALUE:def 1;
then (2 to_power (n - (n * p))) * 2 < (1 / 2) * 2 by XREAL_1:70;
then (2 to_power (n - (n * p))) * (2 to_power 1) < 1 by POWER:30;
then A28: 2 to_power ((n - (n * p)) + 1) < 1 by POWER:32;
1 - p >= 0 by A1, XREAL_1:50;
then n * (1 - p) >= 0 ;
then (n - (n * p)) + 1 >= 0 + 0 ;
then 2 #R ((n - (n * p)) + 1) >= 1 by PREPOWER:99;
hence contradiction by A28, POWER:def 2; :: thesis: verum

end;

hence contradiction ; :: thesis: verum

end;

then not s2 is summable by Th7;
then A29: not s1 is summable by A22, A24, Th35;

now

let n be Element of NAT ; :: thesis: ( n >= 1 implies s . n >= s1 . n )
assume A30: n >= 1 ; :: thesis: s . n >= s1 . n
then s . n = 1 / (n to_power p) by A2
.= s1 . n by A13, A30 ;
hence s . n >= s1 . n ; :: thesis: verum

end;

hence not s is summable by A24, A29, Th22; :: thesis: verum

end;

end;

end;

hence not s is summable ; :: thesis: verum