let s, s1 be Real_Sequence; :: thesis: ( ( for n being Nat holds

( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 < 1 implies s is summable )

assume that

A1: for n being Nat holds

( s . n >= 0 & s1 . n = n -root (s . n) ) and

A2: s1 is convergent and

A3: lim s1 < 1 ; :: thesis: s is summable

0 + (lim s1) < 1 by A3;

then 0 < 1 - (lim s1) by XREAL_1:20;

then (1 - (lim s1)) / 2 > 0 ;

then consider m being Nat such that

A6: for n being Nat st m <= n holds

|.((s1 . n) - (lim s1)).| < (1 - (lim s1)) / 2 by A2, SEQ_2:def 7;

lim (s1 ^\ 1) = lim s1 by A2, SEQ_4:20;

then A7: lim s1 >= 0 by A2, A4, PREPOWER:1;

then 1 + (- (lim s1)) < 1 + 1 by XREAL_1:6;

then (1 - (lim s1)) / 2 < 2 / 2 by XREAL_1:74;

then A8: 1 - ((1 - (lim s1)) / 2) > 0 by XREAL_1:50;

set s2 = (1 - ((1 - (lim s1)) / 2)) GeoSeq ;

A9: ((1 - (lim s1)) / 2) + (lim s1) = 1 - ((1 - (lim s1)) / 2) ;

A10: for n being Nat st m + 1 <= n holds

s . n <= (1 - ((1 - (lim s1)) / 2)) to_power n

s . n <= ((1 - ((1 - (lim s1)) / 2)) GeoSeq) . n

then 1 - (lim s1) < 2 * 2 by XXREAL_0:2;

then (1 - (lim s1)) / 2 < (2 * 2) / 2 by XREAL_1:74;

then (1 - (lim s1)) / 2 < 1 + 1 ;

then ((1 - (lim s1)) / 2) - 1 < 1 by XREAL_1:19;

then A16: - (((1 - (lim s1)) / 2) - 1) > - 1 by XREAL_1:24;

1 - (lim s1) > 0 by A3, XREAL_1:50;

then (1 - (lim s1)) / 2 > 0 ;

then 1 - ((1 - (lim s1)) / 2) < 1 - 0 by XREAL_1:10;

then |.(1 - ((1 - (lim s1)) / 2)).| < 1 by A16, SEQ_2:1;

then (1 - ((1 - (lim s1)) / 2)) GeoSeq is summable by Th24;

hence s is summable by A1, A15, Th19; :: thesis: verum

( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 < 1 implies s is summable )

assume that

A1: for n being Nat holds

( s . n >= 0 & s1 . n = n -root (s . n) ) and

A2: s1 is convergent and

A3: lim s1 < 1 ; :: thesis: s is summable

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

set r = (1 - (lim s1)) / 2;let n be Nat; :: thesis: (s1 ^\ 1) . n >= 0

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

.= (n + 1) -root (s . (n + 1)) by A1 ;

s . (n + 1) >= 0 by A1;

hence (s1 ^\ 1) . n >= 0 by A5, NAT_1:11, POWER:7; :: thesis: verum

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

.= (n + 1) -root (s . (n + 1)) by A1 ;

s . (n + 1) >= 0 by A1;

hence (s1 ^\ 1) . n >= 0 by A5, NAT_1:11, POWER:7; :: thesis: verum

0 + (lim s1) < 1 by A3;

then 0 < 1 - (lim s1) by XREAL_1:20;

then (1 - (lim s1)) / 2 > 0 ;

then consider m being Nat such that

A6: for n being Nat st m <= n holds

|.((s1 . n) - (lim s1)).| < (1 - (lim s1)) / 2 by A2, SEQ_2:def 7;

lim (s1 ^\ 1) = lim s1 by A2, SEQ_4:20;

then A7: lim s1 >= 0 by A2, A4, PREPOWER:1;

then 1 + (- (lim s1)) < 1 + 1 by XREAL_1:6;

then (1 - (lim s1)) / 2 < 2 / 2 by XREAL_1:74;

then A8: 1 - ((1 - (lim s1)) / 2) > 0 by XREAL_1:50;

set s2 = (1 - ((1 - (lim s1)) / 2)) GeoSeq ;

A9: ((1 - (lim s1)) / 2) + (lim s1) = 1 - ((1 - (lim s1)) / 2) ;

A10: for n being Nat st m + 1 <= n holds

s . n <= (1 - ((1 - (lim s1)) / 2)) to_power n

proof

A15:
for n being Nat st m + 1 <= n holds
let n be Nat; :: thesis: ( m + 1 <= n implies s . n <= (1 - ((1 - (lim s1)) / 2)) to_power n )

assume A11: m + 1 <= n ; :: thesis: s . n <= (1 - ((1 - (lim s1)) / 2)) to_power n

1 <= m + 1 by NAT_1:11;

then A12: 1 <= n by A11, XXREAL_0:2;

A13: s . n >= 0 by A1;

m <= n by A11, NAT_1:13;

then |.((s1 . n) - (lim s1)).| < (1 - (lim s1)) / 2 by A6;

then (s1 . n) - (lim s1) < (1 - (lim s1)) / 2 by SEQ_2:1;

then s1 . n < 1 - ((1 - (lim s1)) / 2) by A9, XREAL_1:19;

then A14: n -root (s . n) < 1 - ((1 - (lim s1)) / 2) by A1;

end;assume A11: m + 1 <= n ; :: thesis: s . n <= (1 - ((1 - (lim s1)) / 2)) to_power n

1 <= m + 1 by NAT_1:11;

then A12: 1 <= n by A11, XXREAL_0:2;

A13: s . n >= 0 by A1;

m <= n by A11, NAT_1:13;

then |.((s1 . n) - (lim s1)).| < (1 - (lim s1)) / 2 by A6;

then (s1 . n) - (lim s1) < (1 - (lim s1)) / 2 by SEQ_2:1;

then s1 . n < 1 - ((1 - (lim s1)) / 2) by A9, XREAL_1:19;

then A14: n -root (s . n) < 1 - ((1 - (lim s1)) / 2) by A1;

now :: thesis: s . n < (1 - ((1 - (lim s1)) / 2)) to_power nend;

hence
s . n <= (1 - ((1 - (lim s1)) / 2)) to_power n
; :: thesis: verumper cases
( s . n = 0 or s . n <> 0 )
;

end;

suppose
s . n <> 0
; :: thesis: s . n < (1 - ((1 - (lim s1)) / 2)) to_power n

then
n -Root (s . n) > 0
by A12, A13, PREPOWER:def 2;

then n -root (s . n) > 0 by A12, A13, POWER:def 1;

then (n -root (s . n)) to_power n < (1 - ((1 - (lim s1)) / 2)) to_power n by A11, A14, POWER:37;

hence s . n < (1 - ((1 - (lim s1)) / 2)) to_power n by A12, A13, POWER:4; :: thesis: verum

end;then n -root (s . n) > 0 by A12, A13, POWER:def 1;

then (n -root (s . n)) to_power n < (1 - ((1 - (lim s1)) / 2)) to_power n by A11, A14, POWER:37;

hence s . n < (1 - ((1 - (lim s1)) / 2)) to_power n by A12, A13, POWER:4; :: thesis: verum

s . n <= ((1 - ((1 - (lim s1)) / 2)) GeoSeq) . n

proof

1 - (lim s1) <= 1 - 0
by A7, XREAL_1:6;
let n be Nat; :: thesis: ( m + 1 <= n implies s . n <= ((1 - ((1 - (lim s1)) / 2)) GeoSeq) . n )

((1 - ((1 - (lim s1)) / 2)) GeoSeq) . n = (1 - ((1 - (lim s1)) / 2)) to_power n by PREPOWER:def 1;

hence ( m + 1 <= n implies s . n <= ((1 - ((1 - (lim s1)) / 2)) GeoSeq) . n ) by A10; :: thesis: verum

end;((1 - ((1 - (lim s1)) / 2)) GeoSeq) . n = (1 - ((1 - (lim s1)) / 2)) to_power n by PREPOWER:def 1;

hence ( m + 1 <= n implies s . n <= ((1 - ((1 - (lim s1)) / 2)) GeoSeq) . n ) by A10; :: thesis: verum

then 1 - (lim s1) < 2 * 2 by XXREAL_0:2;

then (1 - (lim s1)) / 2 < (2 * 2) / 2 by XREAL_1:74;

then (1 - (lim s1)) / 2 < 1 + 1 ;

then ((1 - (lim s1)) / 2) - 1 < 1 by XREAL_1:19;

then A16: - (((1 - (lim s1)) / 2) - 1) > - 1 by XREAL_1:24;

1 - (lim s1) > 0 by A3, XREAL_1:50;

then (1 - (lim s1)) / 2 > 0 ;

then 1 - ((1 - (lim s1)) / 2) < 1 - 0 by XREAL_1:10;

then |.(1 - ((1 - (lim s1)) / 2)).| < 1 by A16, SEQ_2:1;

then (1 - ((1 - (lim s1)) / 2)) GeoSeq is summable by Th24;

hence s is summable by A1, A15, Th19; :: thesis: verum