let n be Nat; :: thesis: ( n > 0 implies [\(log 2,(2 * n))/] + 1 <> [\(log 2,((2 * n) + 1))/] )
assume A1: n > 0 ; :: thesis: [\(log 2,(2 * n))/] + 1 <> [\(log 2,((2 * n) + 1))/]
set l22n = log 2,(2 * n);
set l22np1 = log 2,((2 * n) + 1);
A2: 2 * 0 < 2 * n by A1, XREAL_1:70;
assume [\(log 2,(2 * n))/] + 1 = [\(log 2,((2 * n) + 1))/] ; :: thesis: contradiction
then A3: [\((log 2,(2 * n)) + 1)/] = [\(log 2,((2 * n) + 1))/] by INT_1:51;
set k = [\((log 2,(2 * n)) + 1)/];
[\((log 2,(2 * n)) + 1)/] <= log 2,((2 * n) + 1) by A3, INT_1:def 4;
then 2 to_power [\((log 2,(2 * n)) + 1)/] <= 2 to_power (log 2,((2 * n) + 1)) by Th10;
then A4: 2 to_power [\((log 2,(2 * n)) + 1)/] <= (2 * n) + 1 by POWER:def 3;
((log 2,(2 * n)) + 1) - 1 < [\((log 2,(2 * n)) + 1)/] by INT_1:def 4;
then 2 to_power (log 2,(2 * n)) < 2 to_power [\((log 2,(2 * n)) + 1)/] by POWER:44;
then A5: 2 * n < 2 to_power [\((log 2,(2 * n)) + 1)/] by A2, POWER:def 3;
0 + 1 <= (2 * n) + 1 by XREAL_1:9;
then log 2,1 <= log 2,((2 * n) + 1) by Th12;
then 0 <= log 2,((2 * n) + 1) by POWER:59;
then [\0 /] <= [\((log 2,(2 * n)) + 1)/] by A3, Th11;
then 0 <= [\((log 2,(2 * n)) + 1)/] by INT_1:47;
then reconsider k = [\((log 2,(2 * n)) + 1)/] as Element of NAT by INT_1:16;
reconsider 2tpk = 2 |^ k as Element of NAT ;
2 * n < 2tpk by A5, POWER:46;
then A6: (2 * n) + 1 <= 2tpk by NAT_1:13;
2tpk <= (2 * n) + 1 by A4, POWER:46;
then A7: 2tpk = (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:9;
hence contradiction by A1; :: 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 13;
(2 * (2 |^ m)) + 0 = (2 * n) + 1 by A7, A8, NEWTON:11;
then 0 = ((2 * n) + 1) mod 2 by NAT_D:def 2;
hence contradiction by NAT_D:def 2; :: thesis: verum

end;

end;