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 7;
A4: a > 0 by ASYMPT_0:def 1;
then A5: [/a\] > 0 by INT_1:def 7;
then reconsider N = [/a\] as Element of NAT by INT_1:3;
A6: a <> 1 by ASYMPT_0:def 1;

now :: thesis: for n being Nat st n >= N + 1 holds
f . n > 0

A7: log (a,N) >= log (a,a) by A1, A3, PRE_FF:10;
let n be Nat; :: thesis: ( n >= N + 1 implies f . n > 0 )
A8: n in NAT by ORDINAL1:def 12;
assume A9: n >= N + 1 ; :: thesis: f . n > 0
N + 1 > N + 0 by XREAL_1:8;
then n > N by A9, XXREAL_0:2;
then log (a,n) > log (a,N) by A1, A5, POWER:57;
then log (a,n) > 0 by A4, A6, A7, POWER:52;
hence f . n > 0 by A2, A9, A8; :: thesis: verum

end;

hence f is eventually-positive ; :: thesis: verum