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