let n be Element of NAT ; :: thesis: ( n >= 4 implies n * (log (2,n)) >= 2 * n )
assume n >= 4 ; :: thesis: n * (log (2,n)) >= 2 * n
then log (2,n) >= log (2,(2 ^2)) by PRE_FF:12;
then log (2,n) >= log (2,(2 to_power 2)) by POWER:53;
then log (2,n) >= 2 * (log (2,2)) by POWER:63;
then log (2,n) >= 2 * 1 by POWER:60;
hence n * (log (2,n)) >= 2 * n by XREAL_1:66; :: thesis: verum