let a be logbase Real; 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; ( 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)
; 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 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;
( n >= N + 1 implies f . n > 0 )A8:
n in NAT
by ORDINAL1:def 12;
assume A9:
n >= N + 1
;
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;
verum end;
hence
f is eventually-positive
; verum