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 S₁[ 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 A2, XREAL_1:68;
then m * (2 |^ ((n + 1) -' 1)) > n by A1, A3, XXREAL_0:2;
then A4: ex k being Nat st S₁[k] ;
ex k being Nat st
( S₁[k] & ( for j being Nat st S₁[j] holds
k <= j ) ) from NAT_1:sch 5(A4);
then consider k being Nat such that
A5: S₁[k] and
A6: for j being Nat st S₁[j] holds
k <= j ;
( k in NAT & ( for k2 being Element of NAT st k2 < k holds
m * (2 |^ k2) <= n ) ) by A6, ORDINAL1:def 12;
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