let a be real number ; :: thesis: for s being Real_Sequence st 0 < a & a < 1 & ( for n being Element of 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 Element of NAT holds s . n = a to_power (n + 1) ) implies ( s is convergent & lim s = 0 ) )
assume that
A1: ( 0 < a & a < 1 ) and
A2: for n being Element of NAT holds s . n = a to_power (n + 1) ; :: thesis: ( s is convergent & lim s = 0 )
set r = (1 / a) - 1;
1 / a > 1 by A1, Lm1, XREAL_1:90;
then A3: (1 / a) - 1 > 0 by XREAL_1:52;
A4: for p being real number st 0 < p holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - 0 ) < p

proof

let p be real number ; :: thesis: ( 0 < p implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - 0 ) < p )
assume A5: 0 < p ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((s . n) - 0 ) < p
then A6: 1 / p > 0 ;
A7: 1 / (p * ((1 / a) - 1)) = (1 / p) / ((1 / a) - 1) by XCMPLX_1:79;
[\(1 / (p * ((1 / a) - 1)))/] is Element of NAT

proof

p * ((1 / a) - 1) > 0 by A3, A5, XREAL_1:131;
then A8: 1 / (p * ((1 / a) - 1)) > 0 ;
1 / (p * ((1 / a) - 1)) <= [\(1 / (p * ((1 / a) - 1)))/] + 1 by INT_1:52;
hence [\(1 / (p * ((1 / a) - 1)))/] is Element of NAT by A8, INT_1:16, INT_1:20; :: thesis: verum

end;

then consider m being Element of NAT such that
A9: m = [\(1 / (p * ((1 / a) - 1)))/] ;
take m ; :: thesis: for n being Element of NAT st m <= n holds
abs ((s . n) - 0 ) < p

now

let n be Element of NAT ; :: thesis: ( m <= n implies abs ((s . n) - 0 ) < p )
assume A10: m <= n ; :: thesis: abs ((s . n) - 0 ) < p
[\(1 / (p * ((1 / a) - 1)))/] > (1 / (p * ((1 / a) - 1))) - 1 by INT_1:def 4;
then n > (1 / (p * ((1 / a) - 1))) - 1 by A9, A10, XXREAL_0:2;
then n + 1 > (1 / p) / ((1 / a) - 1) by A7, XREAL_1:21;
then A11: (n + 1) * ((1 / a) - 1) > 1 / p by A3, XREAL_1:79;
a to_power (n + 1) > 0 by A1, POWER:39;
then A12: abs (a to_power (n + 1)) = a to_power (n + 1) by ABSVALUE:def 1;
A13: 1 + ((n + 1) * ((1 / a) - 1)) <= (1 + ((1 / a) - 1)) to_power (n + 1) by A3, POWER:56;
A14: (1 + ((1 / a) - 1)) to_power (n + 1) = (1 to_power (n + 1)) / (a to_power (n + 1)) by A1, POWER:36
.= 1 / (a to_power (n + 1)) by POWER:31 ;
0 + ((n + 1) * ((1 / a) - 1)) < 1 + ((n + 1) * ((1 / a) - 1)) by XREAL_1:8;
then 1 / p < 1 + ((n + 1) * ((1 / a) - 1)) by A11, XXREAL_0:2;
then 1 / p < 1 / (a to_power (n + 1)) by A13, A14, XXREAL_0:2;
then abs (a to_power (n + 1)) < p by A6, A12, XREAL_1:93;
hence abs ((s . n) - 0 ) < p by A2; :: thesis: verum

end;

hence for n being Element of NAT st m <= n holds
abs ((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 A4, SEQ_2:def 7; :: thesis: verum