let x be Nat; ex m being Nat st x < 2 to_power m
per cases
( x = 0 or x <> 0 )
;
suppose
x <> 0
;
ex m being Nat st x < 2 to_power mthen
0 < x
;
then P2:
2
to_power (log (2,x)) = x
by POWER:def 3;
X1:
log (2,
x)
<= |.(log (2,x)).|
by COMPLEX1:76;
0 < [/|.(log (2,x)).|\] + 1
by INT_1:32;
then reconsider m =
[/|.(log (2,x)).|\] + 1 as
Nat by INT_1:3, ORDINAL1:def 12;
P3:
log (2,
x)
< m
by X1, INT_1:32, XXREAL_0:2;
take
m
;
x < 2 to_power mthus
x < 2
to_power m
by P2, P3, POWER:39;
verum end; end;