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 PRE_FF:10, AS, NAT_1:23;
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 POWER:56, AS;
then 4 * (log (2,x)) < (n / ((log (x,n)) * (log (2,x)))) * (log (2,x)) by AS2, XREAL_1:68, CL1;
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 XCMPLX_1:106, AS2;
4 * 1 <= 4 * (log (2,x)) by XREAL_1:64, AS2;
hence 4 < n / (log (x,n)) by TT11, XXREAL_0:2; :: thesis: verum