let d be Integer; :: thesis: ex n being non zero Nat st 2 to_power (n - 1) > d

per cases ( d <= 0 or d > 0 ) ;

suppose A1: d <= 0 ; :: thesis: ex n being non zero Nat st 2 to_power (n - 1) > d

take n = 1; :: thesis: 2 to_power (n - 1) > d
thus 2 to_power (n - 1) > d by A1, POWER:24; :: thesis: verum

end;

suppose A2: d > 0 ; :: thesis: ex n being non zero Nat st 2 to_power (n - 1) > d

then d >= 1 + 0 by INT_1:7;

per cases then ( d = 1 or d > 1 ) by XXREAL_0:1;

suppose A3: d = 1 ; :: thesis: ex n being non zero Nat st 2 to_power (n - 1) > d

take n = 2; :: thesis: 2 to_power (n - 1) > d
2 to_power (n - 1) = 2 to_power 1
.= 2 ;
hence 2 to_power (n - 1) > d by A3; :: thesis: verum

end;

suppose d > 1 ; :: thesis: ex n being non zero Nat st 2 to_power (n - 1) > d

then log (2,d) > 0 by ENTROPY1:4;
then A4: [/(log (2,d))\] > 0 by INT_1:def 7;
set n = [/(log (2,d))\] + 2;
[/(log (2,d))\] + 2 in NAT by A4, INT_1:3;
then reconsider n = [/(log (2,d))\] + 2 as Nat ;
reconsider n = n as non zero Nat by A4;
take n ; :: thesis: 2 to_power (n - 1) > d
n - 1 = [/(log (2,d))\] + 1 ;
then 2 to_power (n - 1) > 2 to_power (log (2,d)) by POWER:39, INT_1:32;
hence 2 to_power (n - 1) > d by A2, POWER:def 3; :: thesis: verum

end;

end;

end;

end;