let n be Nat; ( 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
; [\(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 Th10;
log (2,(2 * (2 * n))) =
(log (2,2)) + (log (2,(2 * n)))
by A1, POWER:53
.=
(log (2,(2 * n))) + 1
by POWER:52
;
then
[\(log (2,((2 * n) + 1)))/] <= [\((log (2,(2 * n))) + 1)/]
by A2, Th9;
hence
[\(log (2,(2 * n)))/] + 1 >= [\(log (2,((2 * n) + 1)))/]
by INT_1:28; verum