set r = 1 / 2;

let X be infinite Subset of NAT; :: thesis: for i being Nat holds (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2))

let i be Nat; :: thesis: (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2))

defpred S_{1}[ Nat] means (Partial_Sums (X -powers (1 / 2))) . i <= (Partial_Sums (X -powers (1 / 2))) . (i + $1);

not X c= i + 1 ;

then consider a being object such that

A1: a in X and

A2: not a in i + 1 ;

reconsider a = a, j = i as Element of NAT by A1, ORDINAL1:def 12;

A3: (X -powers (1 / 2)) . a = (1 / 2) |^ a by A1, Def5;

then j + 1 <= a by NAT_1:39;

then consider k being Nat such that

A8: a = (j + 1) + k by NAT_1:10;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

(1 / 2) |^ a > 0 by PREPOWER:6;

then A9: ((Partial_Sums (X -powers (1 / 2))) . i) + ((1 / 2) |^ a) > ((Partial_Sums (X -powers (1 / 2))) . i) + 0 by XREAL_1:6;

A10: S_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A10, A5);

then A11: (Partial_Sums (X -powers (1 / 2))) . i <= (Partial_Sums (X -powers (1 / 2))) . (i + k) ;

j + (k + 1) = (j + k) + 1 ;

then (Partial_Sums (X -powers (1 / 2))) . a = ((Partial_Sums (X -powers (1 / 2))) . (j + k)) + ((1 / 2) |^ a) by A3, A8, SERIES_1:def 1;

then ((Partial_Sums (X -powers (1 / 2))) . i) + ((1 / 2) |^ a) <= (Partial_Sums (X -powers (1 / 2))) . a by A11, XREAL_1:6;

then A12: (Partial_Sums (X -powers (1 / 2))) . i < (Partial_Sums (X -powers (1 / 2))) . a by A9, XXREAL_0:2;

(Partial_Sums (X -powers (1 / 2))) . a <= Sum (X -powers (1 / 2)) by Th21, A4, IRRAT_1:29;

hence (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2)) by A12, XXREAL_0:2; :: thesis: verum

let X be infinite Subset of NAT; :: thesis: for i being Nat holds (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2))

let i be Nat; :: thesis: (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2))

defpred S

not X c= i + 1 ;

then consider a being object such that

A1: a in X and

A2: not a in i + 1 ;

reconsider a = a, j = i as Element of NAT by A1, ORDINAL1:def 12;

A3: (X -powers (1 / 2)) . a = (1 / 2) |^ a by A1, Def5;

A4: now :: thesis: for n being Nat holds 0 <= (X -powers (1 / 2)) . n

let n be Nat; :: thesis: 0 <= (X -powers (1 / 2)) . n

( ( n in X & (X -powers (1 / 2)) . n = (1 / 2) |^ n ) or ( not n in X & (X -powers (1 / 2)) . n = 0 ) ) by Def5;

hence 0 <= (X -powers (1 / 2)) . n by PREPOWER:6; :: thesis: verum

end;( ( n in X & (X -powers (1 / 2)) . n = (1 / 2) |^ n ) or ( not n in X & (X -powers (1 / 2)) . n = 0 ) ) by Def5;

hence 0 <= (X -powers (1 / 2)) . n by PREPOWER:6; :: thesis: verum

A5: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

Segm (j + 1) c= Segm a
by A2, ORDINAL1:16;S

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A6: S_{1}[k]
; :: thesis: S_{1}[k + 1]

i + (k + 1) = (i + k) + 1 ;

then A7: (Partial_Sums (X -powers (1 / 2))) . (j + (k + 1)) = ((Partial_Sums (X -powers (1 / 2))) . (j + k)) + ((X -powers (1 / 2)) . (j + (k + 1))) by SERIES_1:def 1;

(X -powers (1 / 2)) . (j + (k + 1)) >= 0 by A4;

then ((Partial_Sums (X -powers (1 / 2))) . (j + k)) + 0 <= (Partial_Sums (X -powers (1 / 2))) . (j + (k + 1)) by A7, XREAL_1:6;

hence S_{1}[k + 1]
by A6, XXREAL_0:2; :: thesis: verum

end;assume A6: S

i + (k + 1) = (i + k) + 1 ;

then A7: (Partial_Sums (X -powers (1 / 2))) . (j + (k + 1)) = ((Partial_Sums (X -powers (1 / 2))) . (j + k)) + ((X -powers (1 / 2)) . (j + (k + 1))) by SERIES_1:def 1;

(X -powers (1 / 2)) . (j + (k + 1)) >= 0 by A4;

then ((Partial_Sums (X -powers (1 / 2))) . (j + k)) + 0 <= (Partial_Sums (X -powers (1 / 2))) . (j + (k + 1)) by A7, XREAL_1:6;

hence S

then j + 1 <= a by NAT_1:39;

then consider k being Nat such that

A8: a = (j + 1) + k by NAT_1:10;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

(1 / 2) |^ a > 0 by PREPOWER:6;

then A9: ((Partial_Sums (X -powers (1 / 2))) . i) + ((1 / 2) |^ a) > ((Partial_Sums (X -powers (1 / 2))) . i) + 0 by XREAL_1:6;

A10: S

for k being Nat holds S

then A11: (Partial_Sums (X -powers (1 / 2))) . i <= (Partial_Sums (X -powers (1 / 2))) . (i + k) ;

j + (k + 1) = (j + k) + 1 ;

then (Partial_Sums (X -powers (1 / 2))) . a = ((Partial_Sums (X -powers (1 / 2))) . (j + k)) + ((1 / 2) |^ a) by A3, A8, SERIES_1:def 1;

then ((Partial_Sums (X -powers (1 / 2))) . i) + ((1 / 2) |^ a) <= (Partial_Sums (X -powers (1 / 2))) . a by A11, XREAL_1:6;

then A12: (Partial_Sums (X -powers (1 / 2))) . i < (Partial_Sums (X -powers (1 / 2))) . a by A9, XXREAL_0:2;

(Partial_Sums (X -powers (1 / 2))) . a <= Sum (X -powers (1 / 2)) by Th21, A4, IRRAT_1:29;

hence (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2)) by A12, XXREAL_0:2; :: thesis: verum