let p be Real; :: thesis: for s being Real_Sequence st p <= 1 & ( for n being 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 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 Nat st n >= 1 holds

s . n = 1 / (n to_power p) ; :: thesis: not s is summable

s . n = 1 / (n to_power p) ) holds

not s is summable

let s be Real_Sequence; :: thesis: ( p <= 1 & ( for n being 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 Nat st n >= 1 holds

s . n = 1 / (n to_power p) ; :: thesis: not s is summable

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

end;

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

end;

now :: thesis: ( s is convergent implies not lim s = 0 )

hence
not s is summable
by Th4; :: thesis: verumassume
( s is convergent & lim s = 0 )
; :: thesis: contradiction

then consider m being Nat such that

A4: for n being Nat st n >= m holds

|.((s . n) - 0).| < 1 by SEQ_2:def 7;

consider k being Nat such that

A5: k > m by SEQ_4:3;

end;then consider m being Nat such that

A4: for n being Nat st n >= m holds

|.((s . n) - 0).| < 1 by SEQ_2:def 7;

consider k being Nat such that

A5: k > m by SEQ_4:3;

now :: thesis: for n being Nat holds not n >= k

hence
contradiction
; :: thesis: verumlet n be 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 |.((s . n) - 0).| < 1 by A4;

then |.(1 / (n to_power p)).| < 1 by A2, A8;

then |.(n to_power (- p)).| < 1 by A7, POWER:28;

then A9: n to_power (- p) < 1 by ABSVALUE:def 1;

n #R (- p) >= 1 by A3, A8, PREPOWER:85;

hence contradiction by A7, A9, POWER:def 2; :: thesis: verum

end;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 |.((s . n) - 0).| < 1 by A4;

then |.(1 / (n to_power p)).| < 1 by A2, A8;

then |.(n to_power (- p)).| < 1 by A7, POWER:28;

then A9: n to_power (- p) < 1 by ABSVALUE:def 1;

n #R (- p) >= 1 by A3, A8, PREPOWER:85;

hence contradiction by A7, A9, POWER:def 2; :: thesis: verum

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

defpred S_{1}[ Element of NAT , Real] means ( ( $1 = 0 & $2 = 1 ) or ( $1 >= 1 & $2 = 1 / ($1 to_power p) ) );

A11: for n being Element of NAT ex r being Element of REAL st S_{1}[n,r]

A15: for n being Element of NAT holds S_{1}[n,s1 . n]
from FUNCT_2:sch 3(A11);

A16: s1 . 0 = 1 by A15;

_{1}( Nat) -> set = (2 to_power $1) * (s1 . (2 to_power $1));

consider s2 being Real_Sequence such that

A28: for n being Nat holds s2 . n = H_{1}(n)
from SEQ_1:sch 1();

then not s1 is summable by A24, A29, Th31;

hence not s is summable by A29, A25, Th19; :: thesis: verum

end;A11: for n being Element of NAT ex r being Element of REAL st S

proof

consider s1 being Real_Sequence such that
let n be Element of NAT ; :: thesis: ex r being Element of REAL st S_{1}[n,r]

A12: ( n <> 0 implies n >= 0 + 1 ) by NAT_1:13;

end;A12: ( n <> 0 implies n >= 0 + 1 ) by NAT_1:13;

per cases
( n = 0 or n > 0 )
;

end;

suppose A13:
n = 0
; :: thesis: ex r being Element of REAL st S_{1}[n,r]

reconsider jj = 1 as Real ;

take jj ; :: thesis: ( jj is set & jj is Element of REAL & S_{1}[n,jj] )

thus ( jj is set & jj is Element of REAL & S_{1}[n,jj] )
by A13, Lm2; :: thesis: verum

end;take jj ; :: thesis: ( jj is set & jj is Element of REAL & S

thus ( jj is set & jj is Element of REAL & S

suppose A14:
n > 0
; :: thesis: ex r being Element of REAL st S_{1}[n,r]

reconsider n1 = 1 / (n to_power p) as Element of REAL by XREAL_0:def 1;

take n1 ; :: thesis: S_{1}[n,n1]

thus S_{1}[n,n1]
by A14, A12; :: thesis: verum

end;take n1 ; :: thesis: S

thus S

A15: for n being Element of NAT holds S

A16: s1 . 0 = 1 by A15;

now :: thesis: for n being Nat holds s1 . (n + 1) <= s1 . n

then A24:
s1 is V48()
;let n be Nat; :: thesis: s1 . (n + 1) <= s1 . n

end;now :: thesis: s1 . (n + 1) <= s1 . nend;

hence
s1 . (n + 1) <= s1 . n
; :: thesis: verumper cases
( n = 0 or ex m being Nat st n = m + 1 )
by NAT_1:6;

end;

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

then
(n + 1) #R p >= 1
by A10, PREPOWER:85;

then A18: (n + 1) to_power p >= 1 by POWER:def 2;

s1 . (n + 1) = 1 / ((n + 1) to_power p) by A15;

hence s1 . (n + 1) <= s1 . n by A16, A17, A18, XREAL_1:211; :: thesis: verum

end;then A18: (n + 1) to_power p >= 1 by POWER:def 2;

s1 . (n + 1) = 1 / ((n + 1) to_power p) by A15;

hence s1 . (n + 1) <= s1 . n by A16, A17, A18, XREAL_1:211; :: thesis: verum

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

A20:
n in NAT
by ORDINAL1:def 12;

n to_power p > 0 by POWER:34, A19;

then 1 / (n to_power p) > 0 ;

then A21: s1 . n > 0 by A15, A20;

A22: n / (n + 1) <= 1 by NAT_1:11, XREAL_1:183;

A23: n / (n + 1) > 0 by A19;

(s1 . (n + 1)) / (s1 . n) = (1 / ((n + 1) to_power p)) / (s1 . n) by A15

.= (1 / ((n + 1) to_power p)) / (1 / (n to_power p)) by A15, A19

.= (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 A19, POWER:31

.= (n / (n + 1)) #R p by A23, POWER:def 2 ;

then (s1 . (n + 1)) / (s1 . n) <= (n / (n + 1)) #R 0 by A10, A23, A22, PREPOWER:84;

then (s1 . (n + 1)) / (s1 . n) <= 1 by A19, PREPOWER:71;

hence s1 . (n + 1) <= s1 . n by A21, XREAL_1:187; :: thesis: verum

end;n to_power p > 0 by POWER:34, A19;

then 1 / (n to_power p) > 0 ;

then A21: s1 . n > 0 by A15, A20;

A22: n / (n + 1) <= 1 by NAT_1:11, XREAL_1:183;

A23: n / (n + 1) > 0 by A19;

(s1 . (n + 1)) / (s1 . n) = (1 / ((n + 1) to_power p)) / (s1 . n) by A15

.= (1 / ((n + 1) to_power p)) / (1 / (n to_power p)) by A15, A19

.= (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 A19, POWER:31

.= (n / (n + 1)) #R p by A23, POWER:def 2 ;

then (s1 . (n + 1)) / (s1 . n) <= (n / (n + 1)) #R 0 by A10, A23, A22, PREPOWER:84;

then (s1 . (n + 1)) / (s1 . n) <= 1 by A19, PREPOWER:71;

hence s1 . (n + 1) <= s1 . n by A21, XREAL_1:187; :: thesis: verum

A25: now :: thesis: for n being Nat st n >= 1 holds

s . n >= s1 . n

deffunc Hs . n >= s1 . n

let n be Nat; :: thesis: ( n >= 1 implies s . n >= s1 . n )

A26: n in NAT by ORDINAL1:def 12;

assume A27: n >= 1 ; :: thesis: s . n >= s1 . n

then s . n = 1 / (n to_power p) by A2

.= s1 . n by A15, A27, A26 ;

hence s . n >= s1 . n ; :: thesis: verum

end;A26: n in NAT by ORDINAL1:def 12;

assume A27: n >= 1 ; :: thesis: s . n >= s1 . n

then s . n = 1 / (n to_power p) by A2

.= s1 . n by A15, A27, A26 ;

hence s . n >= s1 . n ; :: thesis: verum

consider s2 being Real_Sequence such that

A28: for n being Nat holds s2 . n = H

A29: now :: thesis: for n being Nat holds

( s1 . n >= 0 & s2 . n = (2 to_power n) * (s1 . (2 to_power n)) )

( s1 . n >= 0 & s2 . n = (2 to_power n) * (s1 . (2 to_power n)) )

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

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

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

now :: thesis: ( s2 is convergent implies not lim s2 = 0 )

then
not s2 is summable
by Th4;assume
( s2 is convergent & lim s2 = 0 )
; :: thesis: contradiction

then consider m being Nat such that

A32: for n being Nat st n >= m holds

|.((s2 . n) - 0).| < 1 / 2 by SEQ_2:def 7;

end;then consider m being Nat such that

A32: for n being Nat st n >= m holds

|.((s2 . n) - 0).| < 1 / 2 by SEQ_2:def 7;

now :: thesis: for n being Nat holds not n >= m

hence
contradiction
; :: thesis: verumlet n be Nat; :: thesis: not n >= m

assume n >= m ; :: thesis: contradiction

then |.((s2 . n) - 0).| < 1 / 2 by A32;

then A33: |.((2 to_power n) * (s1 . (2 to_power n))).| < 1 / 2 by A28;

2 to_power n >= 1 by PREPOWER:11;

then |.((2 to_power n) * (1 / ((2 to_power n) to_power p))).| < 1 / 2 by A15, A33;

then |.((2 to_power n) * (1 / (2 to_power (n * p)))).| < 1 / 2 by POWER:33;

then |.((2 to_power n) * (2 to_power (- (n * p)))).| < 1 / 2 by POWER:28;

then |.(2 to_power (n + (- (n * p)))).| < 1 / 2 by POWER:27;

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:68;

then (2 to_power (n - (n * p))) * (2 to_power 1) < 1 ;

then A34: 2 to_power ((n - (n * p)) + 1) < 1 by POWER:27;

1 - p >= 0 by A1, XREAL_1:48;

then n * (1 - p) >= 0 ;

then 2 #R ((n - (n * p)) + 1) >= 1 by PREPOWER:85;

hence contradiction by A34, POWER:def 2; :: thesis: verum

end;assume n >= m ; :: thesis: contradiction

then |.((s2 . n) - 0).| < 1 / 2 by A32;

then A33: |.((2 to_power n) * (s1 . (2 to_power n))).| < 1 / 2 by A28;

2 to_power n >= 1 by PREPOWER:11;

then |.((2 to_power n) * (1 / ((2 to_power n) to_power p))).| < 1 / 2 by A15, A33;

then |.((2 to_power n) * (1 / (2 to_power (n * p)))).| < 1 / 2 by POWER:33;

then |.((2 to_power n) * (2 to_power (- (n * p)))).| < 1 / 2 by POWER:28;

then |.(2 to_power (n + (- (n * p)))).| < 1 / 2 by POWER:27;

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:68;

then (2 to_power (n - (n * p))) * (2 to_power 1) < 1 ;

then A34: 2 to_power ((n - (n * p)) + 1) < 1 by POWER:27;

1 - p >= 0 by A1, XREAL_1:48;

then n * (1 - p) >= 0 ;

then 2 #R ((n - (n * p)) + 1) >= 1 by PREPOWER:85;

hence contradiction by A34, POWER:def 2; :: thesis: verum

then not s1 is summable by A24, A29, Th31;

hence not s is summable by A29, A25, Th19; :: thesis: verum