let s, s1 be Real_Sequence; ( ( 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
; 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 S1[ Nat] means s . (m + $1) <= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + $1);
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 S1[k] holds
S1[k + 1]
(((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:
S1[ 0 ]
;
A16:
for k being Nat holds S1[k]
from NAT_1:sch 2(A15, A9);
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; verum