let n be Nat; :: thesis: ( n > 0 implies [\(log 2,(2 * n))/] + 1 >= [\(log 2,((2 * n) + 1))/] )
set l22n = log 2,(2 * n);
set l22np1 = log 2,((2 * n) + 1);
assume A1: n > 0 ; :: thesis: [\(log 2,(2 * n))/] + 1 >= [\(log 2,((2 * n) + 1))/]
then 0 + 1 <= n by NAT_1:13;
then 1 < (1 * n) + n by XREAL_1:10;
then (2 * n) + 1 < (2 * n) + (2 * n) by XREAL_1:10;
then A2: log 2,((2 * n) + 1) <= log 2,(2 * (2 * n)) by Th12;
2 * 0 < 2 * n by A1, XREAL_1:70;
then log 2,(2 * (2 * n)) = (log 2,2) + (log 2,(2 * n)) by POWER:61
.= (log 2,(2 * n)) + 1 by POWER:60 ;
then [\(log 2,((2 * n) + 1))/] <= [\((log 2,(2 * n)) + 1)/] by A2, Th11;
hence [\(log 2,(2 * n))/] + 1 >= [\(log 2,((2 * n) + 1))/] by INT_1:51; :: thesis: verum