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 )
;

end;

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;thus 2 to_power (n - 1) > d by A1, POWER:24; :: thesis: verum

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;

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

end;

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;2 to_power (n - 1) = 2 to_power 1

.= 2 ;

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

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;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