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

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