let a be Real; for s being Real_Sequence st 0 < a & a < 1 & ( for n being Nat holds s . n = a to_power (n + 1) ) holds
( s is convergent & lim s = 0 )
let s be Real_Sequence; ( 0 < a & a < 1 & ( for n being Nat holds s . n = a to_power (n + 1) ) implies ( s is convergent & lim s = 0 ) )
assume that
A1:
0 < a
and
A2:
a < 1
and
A3:
for n being Nat holds s . n = a to_power (n + 1)
; ( s is convergent & lim s = 0 )
set r = (1 / a) - 1;
1 / a > 1 / 1
by A1, A2, XREAL_1:88;
then A4:
(1 / a) - 1 > 0
by XREAL_1:50;
A5:
for p being Real st 0 < p holds
ex m being Nat st
for n being Nat st m <= n holds
|.((s . n) - 0).| < p
proof
let p be
Real;
( 0 < p implies ex m being Nat st
for n being Nat st m <= n holds
|.((s . n) - 0).| < p )
A6:
1
/ (p * ((1 / a) - 1)) <= [\(1 / (p * ((1 / a) - 1)))/] + 1
by INT_1:29;
assume A7:
0 < p
;
ex m being Nat st
for n being Nat st m <= n holds
|.((s . n) - 0).| < p
then
p * ((1 / a) - 1) > 0
by A4;
then
1
/ (p * ((1 / a) - 1)) > 0
;
then
0 < [\(1 / (p * ((1 / a) - 1)))/] + 1
by A6;
then
[\(1 / (p * ((1 / a) - 1)))/] is
Element of
NAT
by INT_1:3, INT_1:7;
then consider m being
Nat such that A8:
m = [\(1 / (p * ((1 / a) - 1)))/]
;
take
m
;
for n being Nat st m <= n holds
|.((s . n) - 0).| < p
A9:
1
/ (p * ((1 / a) - 1)) = (1 / p) / ((1 / a) - 1)
by XCMPLX_1:78;
now for n being Nat st m <= n holds
|.((s . n) - 0).| < pA10:
[\(1 / (p * ((1 / a) - 1)))/] > (1 / (p * ((1 / a) - 1))) - 1
by INT_1:def 6;
let n be
Nat;
( m <= n implies |.((s . n) - 0).| < p )assume
m <= n
;
|.((s . n) - 0).| < pthen
n > (1 / (p * ((1 / a) - 1))) - 1
by A8, A10, XXREAL_0:2;
then
n + 1
> (1 / p) / ((1 / a) - 1)
by A9, XREAL_1:19;
then A11:
(n + 1) * ((1 / a) - 1) > 1
/ p
by A4, XREAL_1:77;
0 + ((n + 1) * ((1 / a) - 1)) < 1
+ ((n + 1) * ((1 / a) - 1))
by XREAL_1:6;
then A12:
1
/ p < 1
+ ((n + 1) * ((1 / a) - 1))
by A11, XXREAL_0:2;
A13:
(1 + ((1 / a) - 1)) to_power (n + 1) =
(1 to_power (n + 1)) / (a to_power (n + 1))
by A1, POWER:31
.=
1
/ (a to_power (n + 1))
;
a to_power (n + 1) > 0
by A1, POWER:34;
then A14:
|.(a to_power (n + 1)).| = a to_power (n + 1)
by ABSVALUE:def 1;
1
+ ((n + 1) * ((1 / a) - 1)) <= (1 + ((1 / a) - 1)) to_power (n + 1)
by A4, POWER:49;
then
1
/ p < 1
/ (a to_power (n + 1))
by A13, A12, XXREAL_0:2;
then
|.(a to_power (n + 1)).| < p
by A7, A14, XREAL_1:91;
hence
|.((s . n) - 0).| < p
by A3;
verum end;
hence
for
n being
Nat st
m <= n holds
|.((s . n) - 0).| < p
;
verum
end;
hence
s is convergent
by SEQ_2:def 6; lim s = 0
hence
lim s = 0
by A5, SEQ_2:def 7; verum