let a be Real; :: thesis: 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; :: thesis: ( 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) ; :: thesis: ( 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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 :: thesis: for n being Nat st m <= n holds
|.((s . n) - 0).| < p

A10: [\(1 / (p * ((1 / a) - 1)))/] > (1 / (p * ((1 / a) - 1))) - 1 by INT_1:def 6;
let n be Nat; :: thesis: ( m <= n implies |.((s . n) - 0).| < p )
assume m <= n ; :: thesis: |.((s . n) - 0).| < p
then 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; :: thesis: verum

end;

hence for n being Nat st m <= n holds
|.((s . n) - 0).| < p ; :: thesis: verum

end;

hence s is convergent by SEQ_2:def 6; :: thesis: lim s = 0
hence lim s = 0 by A5, SEQ_2:def 7; :: thesis: verum