let a be logbase Real; :: thesis: for f being Real_Sequence st a > 1 & ( for n being Element of NAT st n > 0 holds
f . n = log a,n ) holds
f is eventually-positive
let f be Real_Sequence; :: thesis: ( a > 1 & ( for n being Element of NAT st n > 0 holds
f . n = log a,n ) implies f is eventually-positive )
assume that
A1: a > 1 and
A2: for n being Element of NAT st n > 0 holds
f . n = log a,n ; :: thesis: f is eventually-positive
set N = [/a\];
A3: [/a\] >= a by INT_1:def 5;
A4: a > 0 by ASYMPT_0:def 3;
then A5: [/a\] > 0 by INT_1:def 5;
then reconsider N = [/a\] as Element of NAT by INT_1:16;
A6: a <> 1 by ASYMPT_0:def 3;

now

A7: log a,N >= log a,a by A1, A3, PRE_FF:12;
let n be Element of NAT ; :: thesis: ( n >= N + 1 implies f . n > 0 )
assume A8: n >= N + 1 ; :: thesis: f . n > 0
N + 1 > N + 0 by XREAL_1:10;
then n > N by A8, XXREAL_0:2;
then log a,n > log a,N by A1, A5, POWER:65;
then log a,n > 0 by A4, A6, A7, POWER:60;
hence f . n > 0 by A2, A8; :: thesis: verum

end;

hence f is eventually-positive by ASYMPT_0:def 6; :: thesis: verum