let x be Nat; :: thesis: for n1, n2 being Nat st 2 to_power n1 <= x & x < 2 to_power (n1 + 1) & 2 to_power n2 <= x & x < 2 to_power (n2 + 1) holds
n1 = n2
let n1, n2 be Nat; :: thesis: ( 2 to_power n1 <= x & x < 2 to_power (n1 + 1) & 2 to_power n2 <= x & x < 2 to_power (n2 + 1) implies n1 = n2 )
assume that
AS1: ( 2 to_power n1 <= x & x < 2 to_power (n1 + 1) ) and
AS2: ( 2 to_power n2 <= x & x < 2 to_power (n2 + 1) ) ; :: thesis: n1 = n2
assume n1 <> n2 ; :: thesis: contradiction
per cases then ( n1 < n2 or n2 < n1 ) by XXREAL_0:1;
suppose n1 < n2 ; :: thesis: contradiction
then P1: n1 + 1 <= n2 by NAT_1:13;
2 to_power (n1 + 1) <= 2 to_power n2
proof
per cases ( n1 + 1 = n2 or n1 + 1 < n2 ) by P1, XXREAL_0:1;
suppose n1 + 1 = n2 ; :: thesis: 2 to_power (n1 + 1) <= 2 to_power n2
hence 2 to_power (n1 + 1) <= 2 to_power n2 ; :: thesis: verum
end;
suppose n1 + 1 < n2 ; :: thesis: 2 to_power (n1 + 1) <= 2 to_power n2
hence 2 to_power (n1 + 1) <= 2 to_power n2 by POWER:39; :: thesis: verum
end;
end;
end;
hence contradiction by AS2, AS1, XXREAL_0:2; :: thesis: verum
end;
suppose n2 < n1 ; :: thesis: contradiction
then P1: n2 + 1 <= n1 by NAT_1:13;
2 to_power (n2 + 1) <= 2 to_power n1
proof
per cases ( n2 + 1 = n1 or n2 + 1 < n1 ) by P1, XXREAL_0:1;
suppose n2 + 1 = n1 ; :: thesis: 2 to_power (n2 + 1) <= 2 to_power n1
hence 2 to_power (n2 + 1) <= 2 to_power n1 ; :: thesis: verum
end;
suppose n2 + 1 < n1 ; :: thesis: 2 to_power (n2 + 1) <= 2 to_power n1
hence 2 to_power (n2 + 1) <= 2 to_power n1 by POWER:39; :: thesis: verum
end;
end;
end;
hence contradiction by AS1, AS2, XXREAL_0:2; :: thesis: verum
end;
end;