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));
set k = [\((log (2,(2 * n))) + 1)/];
((log (2,(2 * n))) + 1) - 1 < [\((log (2,(2 * n))) + 1)/]
by INT_1:def 6;
then A1:
2 to_power (log (2,(2 * n))) < 2 to_power [\((log (2,(2 * n))) + 1)/]
by POWER:39;
assume A2:
n > 0
; [\(log (2,(2 * n)))/] + 1 <> [\(log (2,((2 * n) + 1)))/]
then A3:
2 * n < 2 to_power [\((log (2,(2 * n))) + 1)/]
by A1, POWER:def 3;
assume
[\(log (2,(2 * n)))/] + 1 = [\(log (2,((2 * n) + 1)))/]
; contradiction
then A4:
[\((log (2,(2 * n))) + 1)/] = [\(log (2,((2 * n) + 1)))/]
by INT_1:28;
then
[\((log (2,(2 * n))) + 1)/] <= log (2,((2 * n) + 1))
by INT_1:def 6;
then
2 to_power [\((log (2,(2 * n))) + 1)/] <= 2 to_power (log (2,((2 * n) + 1)))
by Th8;
then A5:
2 to_power [\((log (2,(2 * n))) + 1)/] <= (2 * n) + 1
by POWER:def 3;
0 + 1 <= (2 * n) + 1
by XREAL_1:7;
then
log (2,1) <= log (2,((2 * n) + 1))
by Th10;
then
0 <= log (2,((2 * n) + 1))
by POWER:51;
then
[\0/] <= [\((log (2,(2 * n))) + 1)/]
by A4, Th9;
then
0 <= [\((log (2,(2 * n))) + 1)/]
by INT_1:25;
then reconsider k = [\((log (2,(2 * n))) + 1)/] as Element of NAT by INT_1:3;
reconsider T2tpk = 2 |^ k as Element of NAT ;
2 * n < T2tpk
by A3, POWER:41;
then A6:
(2 * n) + 1 <= T2tpk
by NAT_1:13;
T2tpk <= (2 * n) + 1
by A5, POWER:41;
then A7:
T2tpk = (2 * n) + 1
by A6, XXREAL_0:1;