let s, s1 be Real_Sequence; :: thesis: ( ( for n being Nat holds
( s . n > 0 & s1 . n = (s . (n + 1)) / (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 = (s . (n + 1)) / (s . n) ) and
A2: s1 is convergent and
A3: lim s1 < 1 ; :: thesis: s is summable
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
A4: for n being Nat st m <= n holds
|.((s1 . n) - (lim s1)).| < (1 - (lim s1)) / 2 by A2, SEQ_2:def 7;
set s2 = ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq);
defpred S₁[ Nat] means s . (m + $1) <= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + $1);

A5: now :: thesis: for n being Nat holds s1 . n >= 0

let n be Nat; :: thesis: s1 . n >= 0
( s . n > 0 & s . (n + 1) > 0 ) by A1;
then (s . (n + 1)) / (s . n) > 0 ;
hence s1 . n >= 0 by A1; :: thesis: verum

end;

then A6: lim s1 >= 0 by A2, PREPOWER:1;
then 1 + (- (lim s1)) < 1 + 1 by XREAL_1:6;
then A7: (1 - (lim s1)) / 2 < 2 / 2 by XREAL_1:74;
A8: ((1 - (lim s1)) / 2) + (lim s1) = 1 - ((1 - (lim s1)) / 2) ;
A9: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

set X = (s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m));
let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A10: s . (m + k) <= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + k) ; :: thesis: S₁[k + 1]
|.((s1 . (m + k)) - (lim s1)).| < (1 - (lim s1)) / 2 by A4, NAT_1:11;
then (s1 . (m + k)) - (lim s1) < (1 - (lim s1)) / 2 by SEQ_2:1;
then A11: s1 . (m + k) <= 1 - ((1 - (lim s1)) / 2) by A8, XREAL_1:19;
(((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + k) >= 0 by A1, A10;
then A12: (s1 . (m + k)) * ((((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + k)) <= (1 - ((1 - (lim s1)) / 2)) * ((((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + k)) by A11, XREAL_1:64;
s . (m + k) <> 0 by A1;
then A13: s . (m + (k + 1)) = ((s . ((m + k) + 1)) / (s . (m + k))) * (s . (m + k)) by XCMPLX_1:87
.= (s1 . (m + k)) * (s . (m + k)) by A1 ;
s1 . (m + k) >= 0 by A5;
then A14: s . (m + (k + 1)) <= (s1 . (m + k)) * ((((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + k)) by A10, A13, XREAL_1:64;
(1 - ((1 - (lim s1)) / 2)) * ((((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + k)) = (1 - ((1 - (lim s1)) / 2)) * (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) * (((1 - ((1 - (lim s1)) / 2)) GeoSeq) . (m + k))) by SEQ_1:9
.= ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) * ((((1 - ((1 - (lim s1)) / 2)) GeoSeq) . (m + k)) * (1 - ((1 - (lim s1)) / 2)))
.= ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) * (((1 - ((1 - (lim s1)) / 2)) GeoSeq) . ((m + k) + 1)) by PREPOWER:3
.= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + (k + 1)) by SEQ_1:9 ;
hence S₁[k + 1] by A14, A12, XXREAL_0:2; :: thesis: verum

end;

(((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + 0) = ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) * (((1 - ((1 - (lim s1)) / 2)) GeoSeq) . m) by SEQ_1:9
.= ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) * ((1 - ((1 - (lim s1)) / 2)) |^ m) by PREPOWER:def 1
.= (s . m) * (((1 - ((1 - (lim s1)) / 2)) to_power (- m)) * ((1 - ((1 - (lim s1)) / 2)) to_power m))
.= (s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power ((- m) + m)) by A7, POWER:27, XREAL_1:50
.= (s . m) * 1 by POWER:24
.= s . (m + 0) ;
then A15: S₁[ 0 ] ;
A16: for k being Nat holds S₁[k] from NAT_1:sch 2(A15, A9);

A17: now :: thesis: for n being Nat st m <= n holds
s . n <= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . n

let n be Nat; :: thesis: ( m <= n implies s . n <= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . n )
assume m <= n ; :: thesis: s . n <= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . n
then consider k being Nat such that
A18: n = m + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
n = m + k by A18;
hence s . n <= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . n by A16; :: thesis: verum

end;

1 - (lim s1) <= 1 - 0 by A6, 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 A19: - (((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 A19, SEQ_2:1;
then (1 - ((1 - (lim s1)) / 2)) GeoSeq is summable by Th24;
then A20: ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq) is summable by Th10;
for n being Nat holds 0 <= s . n by A1;
hence s is summable by A20, A17, Th19; :: thesis: verum