let n be Nat; ( 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
; [\(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:20;
2 * 0 < 2 * n
by A1, XREAL_1:70;
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; verum