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

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

( 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

hence
s is convergent
by SEQ_2:def 6; :: thesis: lim s = 0
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;

|.((s . n) - 0).| < p ; :: thesis: verum

end;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

hence
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;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

|.((s . n) - 0).| < p ; :: thesis: verum

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