let x be Nat; :: thesis: ex m being Nat st x < 2 to_power m

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

suppose C1: x = 0 ; :: thesis: ex m being Nat st x < 2 to_power m

take m = 0 ; :: thesis: x < 2 to_power m
thus x < 2 to_power m by C1, POWER:24; :: thesis: verum

end;

suppose x <> 0 ; :: thesis: ex m being Nat st x < 2 to_power m

then 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 ; :: thesis: x < 2 to_power m
thus x < 2 to_power m by P2, P3, POWER:39; :: thesis: verum

end;

end;