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

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

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

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

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

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

consider s2 being Real_Sequence such that

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

A9: s1 . 0 = 1 by A7;

_{2}( Nat) -> object = $1 -root (s2 . $1);

consider s3 being Real_Sequence such that

A20: for n being Nat holds s3 . n = H_{2}(n)
from SEQ_1:sch 1();

then lim (s3 ^\ 1) = (s3 ^\ 1) . 0 by SEQ_4:26

.= 2 to_power (1 - p) by A24 ;

then A27: lim s3 = 2 to_power (1 - p) by A26, SEQ_4:22;

1 - p < 0 by A1, XREAL_1:49;

then lim s3 < 1 by A27, POWER:36;

then s2 is summable by A20, A21, A34, Th28;

then s1 is summable by A17, A28, Th31;

then s1 ^\ 1 is summable by Th12;

then s ^\ 1 is summable by A31, A18, Th19;

hence s is summable by Th13; :: thesis: verum

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

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

defpred S

A3: 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]

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

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

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

end;

suppose A5:
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 A5, 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 A6:
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 A6, A4; :: thesis: verum

end;take n1 ; :: thesis: S

thus S

A7: for n being Element of NAT holds S

deffunc H

consider s2 being Real_Sequence such that

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

A9: s1 . 0 = 1 by A7;

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

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

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

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

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

hence s1 . (n + 1) <= s1 . n by A9, A10, A11, XREAL_1:211; :: thesis: verum

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

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

hence s1 . (n + 1) <= s1 . n by A9, A10, A11, XREAL_1:211; :: thesis: verum

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

A13:
n in NAT
by ORDINAL1:def 12;

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

then 1 / (n to_power p) > 0 ;

then A14: s1 . n > 0 by A7, A13;

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

A16: n / (n + 1) > 0 by A12;

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

.= (1 / ((n + 1) to_power p)) / (1 / (n to_power p)) by A7, A12

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

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

then (s1 . (n + 1)) / (s1 . n) <= (n / (n + 1)) #R 0 by A1, A16, A15, PREPOWER:84;

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

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

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

then 1 / (n to_power p) > 0 ;

then A14: s1 . n > 0 by A7, A13;

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

A16: n / (n + 1) > 0 by A12;

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

.= (1 / ((n + 1) to_power p)) / (1 / (n to_power p)) by A7, A12

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

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

then (s1 . (n + 1)) / (s1 . n) <= (n / (n + 1)) #R 0 by A1, A16, A15, PREPOWER:84;

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

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

A18: now :: thesis: for n being Nat st n >= 0 holds

(s1 ^\ 1) . n >= (s ^\ 1) . n

deffunc H(s1 ^\ 1) . n >= (s ^\ 1) . n

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

assume n >= 0 ; :: thesis: (s1 ^\ 1) . n >= (s ^\ 1) . n

A19: n + 1 >= 0 + 1 by XREAL_1:6;

(s ^\ 1) . n = s . (n + 1) by NAT_1:def 3

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

.= s1 . (n + 1) by A7

.= (s1 ^\ 1) . n by NAT_1:def 3 ;

hence (s1 ^\ 1) . n >= (s ^\ 1) . n ; :: thesis: verum

end;assume n >= 0 ; :: thesis: (s1 ^\ 1) . n >= (s ^\ 1) . n

A19: n + 1 >= 0 + 1 by XREAL_1:6;

(s ^\ 1) . n = s . (n + 1) by NAT_1:def 3

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

.= s1 . (n + 1) by A7

.= (s1 ^\ 1) . n by NAT_1:def 3 ;

hence (s1 ^\ 1) . n >= (s ^\ 1) . n ; :: thesis: verum

consider s3 being Real_Sequence such that

A20: for n being Nat holds s3 . n = H

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

( s2 . n = 2 to_power ((1 - p) * n) & s2 . n >= 0 & s3 . n = n -root ((2 to_power (1 - p)) to_power n) )

A0:
2 to_power (1 - p) is set
by TARSKI:1;( s2 . n = 2 to_power ((1 - p) * n) & s2 . n >= 0 & s3 . n = n -root ((2 to_power (1 - p)) to_power n) )

let n be 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) )

A22: 2 to_power n > 0 by POWER:34;

thus A23: s2 . n = (2 to_power n) * (s1 . (2 to_power n)) by A8

.= (2 to_power n) * (1 / ((2 to_power n) to_power p)) by A7, A22

.= (2 to_power n) * (1 / (2 to_power (n * p))) by POWER:33

.= (2 to_power n) * (2 to_power (- (n * p))) by POWER:28

.= 2 to_power (n + (- (n * p))) by POWER:27

.= 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:34; :: thesis: s3 . n = n -root ((2 to_power (1 - p)) to_power n)

s2 . n = (2 to_power (1 - p)) to_power n by A23, POWER:33;

hence s3 . n = n -root ((2 to_power (1 - p)) to_power n) by A20; :: thesis: verum

end;A22: 2 to_power n > 0 by POWER:34;

thus A23: s2 . n = (2 to_power n) * (s1 . (2 to_power n)) by A8

.= (2 to_power n) * (1 / ((2 to_power n) to_power p)) by A7, A22

.= (2 to_power n) * (1 / (2 to_power (n * p))) by POWER:33

.= (2 to_power n) * (2 to_power (- (n * p))) by POWER:28

.= 2 to_power (n + (- (n * p))) by POWER:27

.= 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:34; :: thesis: s3 . n = n -root ((2 to_power (1 - p)) to_power n)

s2 . n = (2 to_power (1 - p)) to_power n by A23, POWER:33;

hence s3 . n = n -root ((2 to_power (1 - p)) to_power n) by A20; :: thesis: verum

A24: now :: thesis: for n being Nat holds (s3 ^\ 1) . n = 2 to_power (1 - p)

then A26:
s3 ^\ 1 is constant
by A0;let n be Nat; :: thesis: (s3 ^\ 1) . n = 2 to_power (1 - p)

A25: ( n + 1 >= 0 + 1 & 2 to_power (1 - p) >= 0 ) by POWER:34, XREAL_1:6;

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 A21

.= 2 to_power (1 - p) by A25, POWER:4 ; :: thesis: verum

end;A25: ( n + 1 >= 0 + 1 & 2 to_power (1 - p) >= 0 ) by POWER:34, XREAL_1:6;

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 A21

.= 2 to_power (1 - p) by A25, POWER:4 ; :: thesis: verum

then lim (s3 ^\ 1) = (s3 ^\ 1) . 0 by SEQ_4:26

.= 2 to_power (1 - p) by A24 ;

then A27: lim s3 = 2 to_power (1 - p) by A26, SEQ_4:22;

A28: 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 A8; :: thesis: verum

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

A31: now :: thesis: for n being Nat holds (s ^\ 1) . n >= 0

A34:
s3 is convergent
by A26, SEQ_4:21;let n be Nat; :: thesis: (s ^\ 1) . n >= 0

A32: n + 1 >= 0 + 1 by XREAL_1:6;

A33: s1 . (n + 1) >= 0 by A28;

(s ^\ 1) . n = s . (n + 1) by NAT_1:def 3

.= 1 / ((n + 1) to_power p) by A2, A32

.= s1 . (n + 1) by A7

.= (s1 ^\ 1) . n by NAT_1:def 3 ;

hence (s ^\ 1) . n >= 0 by A33, NAT_1:def 3; :: thesis: verum

end;A32: n + 1 >= 0 + 1 by XREAL_1:6;

A33: s1 . (n + 1) >= 0 by A28;

(s ^\ 1) . n = s . (n + 1) by NAT_1:def 3

.= 1 / ((n + 1) to_power p) by A2, A32

.= s1 . (n + 1) by A7

.= (s1 ^\ 1) . n by NAT_1:def 3 ;

hence (s ^\ 1) . n >= 0 by A33, NAT_1:def 3; :: thesis: verum

1 - p < 0 by A1, XREAL_1:49;

then lim s3 < 1 by A27, POWER:36;

then s2 is summable by A20, A21, A34, Th28;

then s1 is summable by A17, A28, Th31;

then s1 ^\ 1 is summable by Th12;

then s ^\ 1 is summable by A31, A18, Th19;

hence s is summable by Th13; :: thesis: verum