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
A4: now :: thesis: for n being Nat holds (s1 ^\ 1) . n >= 0
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;
set r = (1 - (lim s1)) / 2;
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
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;
now :: thesis: s . n < (1 - ((1 - (lim s1)) / 2)) to_power n
per cases ( s . n = 0 or s . n <> 0 ) ;
suppose s . n = 0 ; :: thesis: s . n < (1 - ((1 - (lim s1)) / 2)) to_power n
hence s . n < (1 - ((1 - (lim s1)) / 2)) to_power n by A8, POWER:34; :: thesis: verum
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;
end;
end;
hence s . n <= (1 - ((1 - (lim s1)) / 2)) to_power n ; :: thesis: verum
end;
A15: for n being Nat st m + 1 <= n holds
s . n <= ((1 - ((1 - (lim s1)) / 2)) GeoSeq) . n
proof
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 - (lim s1) <= 1 - 0 by A7, XREAL_1:6;
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