let n be 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:10;
then log (2,n) >= log (2,(2 to_power 2)) by POWER:46;
then log (2,n) >= 2 * (log (2,2)) by POWER:55;
then log (2,n) >= 2 * 1 by POWER:52;
hence n * (log (2,n)) >= 2 * n by XREAL_1:64; :: thesis: verum