let n be Nat; ( n >= 4 implies n * (log (2,n)) >= 2 * n )
assume
n >= 4
; 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; verum