let p be Real; 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; ( 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)
; not s is summable
per cases
( p < 0 or p >= 0 )
;
suppose A10:
p >= 0
;
not s is summable defpred S1[
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
S1[
n,
r]
consider s1 being
Real_Sequence such that A15:
for
n being
Element of
NAT holds
S1[
n,
s1 . n]
from FUNCT_2:sch 3(A11);
A16:
s1 . 0 = 1
by A15;
now for n being Nat holds s1 . (n + 1) <= s1 . nlet n be
Nat;
s1 . (n + 1) <= s1 . nnow s1 . (n + 1) <= s1 . nper cases
( n = 0 or ex m being Nat st n = m + 1 )
by NAT_1:6;
suppose A19:
ex
m being
Nat st
n = m + 1
;
s1 . (n + 1) <= s1 . nA20:
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;
verum end; end; end; hence
s1 . (n + 1) <= s1 . n
;
verum end; then A24:
s1 is
V48()
;
A25:
now for n being Nat st n >= 1 holds
s . n >= s1 . nend; deffunc H1(
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 = H1(
n)
from SEQ_1:sch 1();
then
not
s2 is
summable
by Th4;
then
not
s1 is
summable
by A24, A29, Th31;
hence
not
s is
summable
by A29, A25, Th19;
verum end; end;