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_{1}[ 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_{1}[k]
;

ex k being Nat st

( S_{1}[k] & ( for j being Nat st S_{1}[j] holds

k <= j ) ) from NAT_1:sch 5(A4);

then consider k being Nat such that

A5: S_{1}[k]
and

A6: for j being Nat st S_{1}[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

( ( for k2 being Element of NAT st k2 < i holds

m * (2 |^ k2) <= n ) & m * (2 |^ i) > n ) )

defpred S

(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

ex k being Nat st

( S

k <= j ) ) from NAT_1:sch 5(A4);

then consider k being Nat such that

A5: S

A6: for j being Nat st S

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