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));
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 ; :: thesis: [\(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)))/] ; :: thesis: 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;
per cases ( k = 0 or ex m being Nat st k = m + 1 ) by NAT_1:6;
suppose k = 0 ; :: thesis: contradiction
then 1 - 1 = ((2 * n) + 1) - 1 by A7, NEWTON:4;
hence contradiction by A2; :: thesis: verum
end;
suppose ex m being Nat st k = m + 1 ; :: thesis: contradiction
then consider m being Nat such that
A8: k = m + 1 ;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
(2 * (2 |^ m)) + 0 = (2 * n) + 1 by A7, A8, NEWTON:6;
then 0 = ((2 * n) + 1) mod 2 by NAT_D:def 2;
hence contradiction by NAT_D:def 2; :: thesis: verum
end;
end;