let x be Nat; :: thesis: ( 1 < x implies ex N being Nat st
for n being Nat st N <= n holds
4 < n / (log (x,n)) )

assume AS: 1 < x ; :: thesis: ex N being Nat st
for n being Nat st N <= n holds
4 < n / (log (x,n))

log (2,x) >= log (2,2) by ;
then AS2: 1 <= log (2,x) by POWER:52;
consider N being Nat such that
LL1: for n being Nat st N <= n holds
4 < n / (log (2,n)) by LMC31HC;
take N ; :: thesis: for n being Nat st N <= n holds
4 < n / (log (x,n))

let n be Nat; :: thesis: ( N <= n implies 4 < n / (log (x,n)) )
assume N <= n ; :: thesis: 4 < n / (log (x,n))
then CL1: 4 < n / (log (2,n)) by LL1;
then 0 <> n ;
then log (2,n) = (log (2,x)) * (log (x,n)) by ;
then 4 * (log (2,x)) < (n / ((log (x,n)) * (log (2,x)))) * (log (2,x)) by ;
then 4 * (log (2,x)) < ((n / (log (x,n))) * (1 / (log (2,x)))) * (log (2,x)) by XCMPLX_1:103;
then 4 * (log (2,x)) < (n / (log (x,n))) * ((log (2,x)) * (1 / (log (2,x)))) ;
then TT11: 4 * (log (2,x)) < (n / (log (x,n))) * 1 by ;
4 * 1 <= 4 * (log (2,x)) by ;
hence 4 < n / (log (x,n)) by ; :: thesis: verum