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:8;
then (2 * n) + 1 < (2 * n) + (2 * n) by XREAL_1:8;
then A2: log (2,((2 * n) + 1)) <= log (2,(2 * (2 * n))) by Th12;
2 * 0 < 2 * n by A1, XREAL_1:68;
then log (2,(2 * (2 * n))) = (log (2,2)) + (log (2,(2 * n))) by POWER:53
.= (log (2,(2 * n))) + 1 by POWER:52 ;
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:28; :: thesis: verum