let L be Real; :: thesis: ( 0 < L & L < 1 implies for s being Real st 0 < s holds
ex n being Element of NAT st L to_power n < s )
assume A1:
( 0 < L & L < 1 )
; :: thesis: for s being Real st 0 < s holds
ex n being Element of NAT st L to_power n < s
deffunc H1( Element of NAT ) -> Element of REAL = L to_power ($1 + 1);
consider rseq being Real_Sequence such that
A2:
for n being Element of NAT holds rseq . n = H1(n)
from SEQ_1:sch 1();
A3:
( rseq is convergent & lim rseq = 0 )
by A1, A2, SERIES_1:1;
let s be Real; :: thesis: ( 0 < s implies ex n being Element of NAT st L to_power n < s )
assume
0 < s
; :: thesis: ex n being Element of NAT st L to_power n < s
then consider n being Element of NAT such that
A4:
for m being Element of NAT st n <= m holds
abs ((rseq . m) - 0 ) < s
by A3, SEQ_2:def 7;
A5:
0 < L to_power (n + 1)
by A1, Th2;
A6: abs ((rseq . n) - 0 ) =
abs (L to_power (n + 1))
by A2
.=
L to_power (n + 1)
by A5, ABSVALUE:def 1
;
take
n + 1
; :: thesis: L to_power (n + 1) < s
thus
L to_power (n + 1) < s
by A4, A6; :: thesis: verum