ex N being Element of NAT st
for n being Element of NAT st n >= N holds
n / 2 > (log 2,n) * (log 2,n)

proof

reconsider N = 2 to_power 10 as Element of NAT ;

now

take N = N; :: thesis: for n being Element of NAT st n >= N holds
n / 2 > (log 2,n) * (log 2,n)
let n be Element of NAT ; :: thesis: ( n >= N implies n / 2 > (log 2,n) * (log 2,n) )
set x = log 2,n;
A1: 2 to_power 9 > 0 by POWER:39;
assume A2: n >= N ; :: thesis: n / 2 > (log 2,n) * (log 2,n)
then A3: n > 0 by POWER:39;
2 to_power 10 > 2 to_power 0 by POWER:44;
then n > 2 to_power 0 by A2, XXREAL_0:2;
then n > 1 by POWER:29;
then log 2,n > log 2,1 by POWER:65;
then log 2,n > 0 by POWER:59;
then (log 2,n) * (log 2,n) > 0 * (log 2,n) by XREAL_1:70;
then A4: 4 * ((log 2,n) * (log 2,n)) > 2 * ((log 2,n) * (log 2,n)) by XREAL_1:70;
2 to_power 10 > 2 to_power 1 by POWER:44;
then n > 2 to_power 1 by A2, XXREAL_0:2;
then A5: n > 2 by POWER:30;
then A6: 2 * n > 2 * 2 by XREAL_1:70;
n * n > 2 * n by A5, XREAL_1:70;
then n ^2 > 2 * 2 by A6, XXREAL_0:2;
then log 2,(n ^2 ) > log 2,(2 ^2 ) by POWER:65;
then log 2,(n ^2 ) > log 2,(2 to_power 2) by POWER:53;
then log 2,(n ^2 ) > 2 * (log 2,2) by POWER:63;
then A7: log 2,(n ^2 ) > 2 * 1 by POWER:60;
then A8: (log 2,(n ^2 )) ^2 > 0 by SQUARE_1:74;
2 to_power 10 > 2 to_power 9 by POWER:44;
then n > 2 to_power 9 by A2, XXREAL_0:2;
then log 2,n > log 2,(2 to_power 9) by A1, POWER:65;
then log 2,n > 9 * (log 2,2) by POWER:63;
then A9: log 2,n > 9 * 1 by POWER:60;
then A10: 2 * (log 2,n) > 0 * (log 2,n) by XREAL_1:70;
then (2 * (log 2,n)) * (2 * (log 2,n)) > 0 * (2 * (log 2,n)) by XREAL_1:70;
then log 2,(2 to_power (log 2,n)) > log 2,((2 * (log 2,n)) ^2 ) by A9, Lm31, POWER:65;
then (log 2,n) * (log 2,2) > log 2,((2 * (log 2,n)) ^2 ) by POWER:63;
then (log 2,n) * 1 > log 2,((2 * (log 2,n)) ^2 ) by POWER:60;
then log 2,n > log 2,((2 * (log 2,n)) to_power 2) by POWER:53;
then log 2,n > 2 * (log 2,(2 * (log 2,n))) by A10, POWER:63;
then log 2,n > 2 * (log 2,(log 2,(n to_power 2))) by A3, POWER:63;
then log 2,n > 2 * (log 2,(log 2,(n ^2 ))) by POWER:53;
then 2 to_power (log 2,n) > 2 to_power (2 * (log 2,(log 2,(n ^2 )))) by POWER:44;
then n > 2 to_power (2 * (log 2,(log 2,(n ^2 )))) by A3, POWER:def 3;
then n > 2 to_power (log 2,((log 2,(n ^2 )) to_power 2)) by A7, POWER:63;
then n > 2 to_power (log 2,((log 2,(n ^2 )) ^2 )) by POWER:53;
then n > (log 2,(n ^2 )) ^2 by A8, POWER:def 3;
then n > (log 2,(n to_power 2)) ^2 by POWER:53;
then n > (2 * (log 2,n)) ^2 by A3, POWER:63;
then n > 2 * ((log 2,n) * (log 2,n)) by A4, XXREAL_0:2;
hence n / 2 > (log 2,n) * (log 2,n) by XREAL_1:83; :: thesis: verum

end;

hence ex N being Element of NAT st
for n being Element of NAT st n >= N holds
n / 2 > (log 2,n) * (log 2,n) ; :: thesis: verum

end;

then consider N3 being Element of NAT such that
A11: for n being Element of NAT st n >= N3 holds
n / 2 > (log 2,n) * (log 2,n) ;

now

take N = 30; :: thesis: for n being Element of NAT st n >= N holds
n / 3 > 2 * (log 2,n)
let n be Element of NAT ; :: thesis: ( n >= N implies n / 3 > 2 * (log 2,n) )
assume A12: n >= N ; :: thesis: n / 3 > 2 * (log 2,n)
then A13: n to_power 6 > 0 by POWER:39;
2 to_power n > n to_power 6 by A12, Lm30;
then log 2,(2 to_power n) > log 2,(n to_power 6) by A13, POWER:65;
then n * (log 2,2) > log 2,(n to_power 6) by POWER:63;
then n * 1 > log 2,(n to_power 6) by POWER:60;
then n > (3 * 2) * (log 2,n) by A12, POWER:63;
then n > 3 * (2 * (log 2,n)) ;
hence n / 3 > 2 * (log 2,n) by XREAL_1:83; :: thesis: verum

end;

then consider N2 being Element of NAT such that
A14: for n being Element of NAT st n >= N2 holds
n / 3 > 2 * (log 2,n) ;

now

take N = 7; :: thesis: for n being Element of NAT st n >= N holds
n / 6 > 1
let n be Element of NAT ; :: thesis: ( n >= N implies n / 6 > 1 )
assume n >= N ; :: thesis: n / 6 > 1
then n > 6 by XXREAL_0:2;
then n / 6 > 6 / 6 by XREAL_1:76;
hence n / 6 > 1 ; :: thesis: verum

end;

then consider N1 being Element of NAT such that
A15: for n being Element of NAT st n >= N1 holds
n / 6 > 1 ;
set N = max (max N1,2),(max N2,N3);
A16: max (max N1,2),(max N2,N3) >= max N1,2 by XXREAL_0:25;
max N1,2 >= 2 by XXREAL_0:25;
then A17: max (max N1,2),(max N2,N3) >= 2 by A16, XXREAL_0:2;
A18: max (max N1,2),(max N2,N3) >= max N2,N3 by XXREAL_0:25;
max N2,N3 >= N3 by XXREAL_0:25;
then A19: max (max N1,2),(max N2,N3) >= N3 by A18, XXREAL_0:2;
max N2,N3 >= N2 by XXREAL_0:25;
then A20: max (max N1,2),(max N2,N3) >= N2 by A18, XXREAL_0:2;
max N1,2 >= N1 by XXREAL_0:25;
then A21: max (max N1,2),(max N2,N3) >= N1 by A16, XXREAL_0:2;

now

let n be Element of NAT ; :: thesis: ( n >= max (max N1,2),(max N2,N3) implies (sqrt n) - (log 2,n) > 1 )
A22: (1 + (2 * (log 2,n))) + ((log 2,n) * (log 2,n)) = (1 + (log 2,n)) ^2 ;
assume A23: n >= max (max N1,2),(max N2,N3) ; :: thesis: (sqrt n) - (log 2,n) > 1
then n >= N2 by A20, XXREAL_0:2;
then A24: n / 3 > 2 * (log 2,n) by A14;
n >= 2 by A17, A23, XXREAL_0:2;
then log 2,n >= log 2,2 by PRE_FF:12;
then A25: log 2,n >= 1 by POWER:60;
n >= N1 by A21, A23, XXREAL_0:2;
then n / 6 > 1 by A15;
then A26: (n / 6) + (n / 3) > 1 + (2 * (log 2,n)) by A24, XREAL_1:10;
n >= N3 by A19, A23, XXREAL_0:2;
then A27: n / 2 > (log 2,n) * (log 2,n) by A11;
((n / 6) + (n / 3)) + (n / 2) = n ;
then n > (1 + (log 2,n)) ^2 by A26, A27, A22, XREAL_1:10;
then sqrt n > sqrt ((1 + (log 2,n)) ^2 ) by SQUARE_1:95, XREAL_1:65;
then sqrt n > 1 + (log 2,n) by A25, SQUARE_1:89;
hence (sqrt n) - (log 2,n) > 1 by XREAL_1:22; :: thesis: verum

end;

hence ex N being Element of NAT st
for n being Element of NAT st n >= N holds
(sqrt n) - (log 2,n) > 1 ; :: thesis: verum