let n be Nat; :: thesis: ( n > 0 implies [\(log (2,(2 * n)))/] = [\(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)))/] = [\(log (2,((2 * n) + 1)))/]
then ( [\(log (2,((2 * n) + 1)))/] <> [\(log (2,(2 * n)))/] + 1 & [\(log (2,((2 * n) + 1)))/] <= [\(log (2,(2 * n)))/] + 1 ) by Th13, Th14;
then [\(log (2,((2 * n) + 1)))/] < [\(log (2,(2 * n)))/] + 1 by XXREAL_0:1;
then A2: [\(log (2,((2 * n) + 1)))/] <= ([\(log (2,(2 * n)))/] + 1) - 1 by INT_1:7;
2 * 0 < 2 * n by A1, XREAL_1:68;
then log (2,(2 * n)) <= log (2,((2 * n) + 1)) by Th12, NAT_1:11;
then [\(log (2,(2 * n)))/] <= [\(log (2,((2 * n) + 1)))/] by Th11;
hence [\(log (2,(2 * n)))/] = [\(log (2,((2 * n) + 1)))/] by A2, XXREAL_0:1; :: thesis: verum