let a, b be non trivial Nat; :: thesis: ex n being Nat st
( b |^ n <= a & a < b |^ (n + 1) )
reconsider c = log (b,a) as Real ;
A1: b > 1 by NEWTON03:def 1;
b to_power c > 1 by NEWTON03:def 1;
then c >= 0 ;
then [\c/] in NAT by INT_1:3;
then reconsider d = [\c/] as Nat ;
( d <= c & c < d + 1 ) by INT_1:def 6, INT_1:29;
then ( b to_power d <= b to_power c & b to_power c < b to_power (d + 1) ) by POWER:39, PRE_FF:8, A1;
hence ex n being Nat st
( b |^ n <= a & a < b |^ (n + 1) ) ; :: thesis: verum