let m, n be Element of NAT ; :: thesis: ( m > 0 implies ex i being Element of NAT st
( ( for k2 being Element of NAT st k2 < i holds
m * (2 |^ k2) <= n ) & m * (2 |^ i) > n ) )

defpred S1[ Nat] means m * (2 |^ \$1) > n;
(n + 1) - 1 = n ;
then A1: (n + 1) -' 1 = n by XREAL_0:def 2;
assume A2: m > 0 ; :: thesis: ex i being Element of NAT st
( ( for k2 being Element of NAT st k2 < i holds
m * (2 |^ k2) <= n ) & m * (2 |^ i) > n )

then m >= 0 + 1 by NAT_1:13;
then A3: m * n >= 1 * n by XREAL_1:64;
2 |^ ((n + 1) -' 1) > (n + 1) -' 1 by NEWTON:86;
then m * (2 |^ ((n + 1) -' 1)) > m * ((n + 1) -' 1) by ;
then m * (2 |^ ((n + 1) -' 1)) > n by ;
then A4: ex k being Nat st S1[k] ;
ex k being Nat st
( S1[k] & ( for j being Nat st S1[j] holds
k <= j ) ) from then consider k being Nat such that
A5: S1[k] and
A6: for j being Nat st S1[j] holds
k <= j ;
( k in NAT & ( for k2 being Element of NAT st k2 < k holds
m * (2 |^ k2) <= n ) ) by ;
hence ex i being Element of NAT st
( ( for k2 being Element of NAT st k2 < i holds
m * (2 |^ k2) <= n ) & m * (2 |^ i) > n ) by A5; :: thesis: verum