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 and
A2: a < 1 and
A3: 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, A2, Lm1, XREAL_1:88;
then A4: (1 / a) - 1 > 0 by XREAL_1:50;
A5: 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 )
A6: 1 / (p * ((1 / a) - 1)) <= [\(1 / (p * ((1 / a) - 1)))/] + 1 by INT_1:29;
assume A7: 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 p * ((1 / a) - 1) > 0 by A4;
then 1 / (p * ((1 / a) - 1)) > 0 ;
then [\(1 / (p * ((1 / a) - 1)))/] is Element of NAT by A6, INT_1:3, INT_1:7;
then consider m being Element of NAT such that
A8: m = [\(1 / (p * ((1 / a) - 1)))/] ;
take m ; :: thesis: for n being Element of NAT st m <= n holds
abs ((s . n) - 0) < p
A9: 1 / (p * ((1 / a) - 1)) = (1 / p) / ((1 / a) - 1) by XCMPLX_1:78;

now

A10: [\(1 / (p * ((1 / a) - 1)))/] > (1 / (p * ((1 / a) - 1))) - 1 by INT_1:def 6;
let n be Element of NAT ; :: thesis: ( m <= n implies abs ((s . n) - 0) < p )
assume m <= n ; :: thesis: abs ((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)) by POWER:26 ;
a to_power (n + 1) > 0 by A1, POWER:34;
then A14: abs (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 abs (a to_power (n + 1)) < p by A7, A14, XREAL_1:91;
hence abs ((s . n) - 0) < p by A3; :: 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 A5, SEQ_2:def 7; :: thesis: verum