let n be Nat; :: thesis: for p being ExtReal st 0 <= p & p < n holds

ex k being Nat st

( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= p & p < k / (2 |^ n) )

let p be ExtReal; :: thesis: ( 0 <= p & p < n implies ex k being Nat st

( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= p & p < k / (2 |^ n) ) )

assume that

A1: 0 <= p and

A2: p < n ; :: thesis: ex k being Nat st

( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= p & p < k / (2 |^ n) )

0 in REAL by XREAL_0:def 1;

then reconsider p1 = p as Element of REAL by A1, A2, XXREAL_0:46;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

set k = [\((p1 * (2 |^ n)) + 1)/];

A3: ((p1 * (2 |^ n)) + 1) - 1 = p1 * (2 |^ n) ;

then A4: 0 < [\((p1 * (2 |^ n)) + 1)/] by A1, INT_1:def 6;

then reconsider k = [\((p1 * (2 |^ n)) + 1)/] as Element of NAT by INT_1:3;

A5: p1 * (2 |^ n) < k by A3, INT_1:def 6;

A6: 0 < 2 |^ n by PREPOWER:6;

k <= (p1 * (2 |^ n)) + 1 by INT_1:def 6;

then A11: k - 1 <= p1 * (2 |^ n) by XREAL_1:20;

0 + 1 <= k by A4, NAT_1:13;

hence ( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= p & p < k / (2 |^ n) ) by A6, A7, A5, A11, XREAL_1:79, XREAL_1:81; :: thesis: verum

ex k being Nat st

( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= p & p < k / (2 |^ n) )

let p be ExtReal; :: thesis: ( 0 <= p & p < n implies ex k being Nat st

( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= p & p < k / (2 |^ n) ) )

assume that

A1: 0 <= p and

A2: p < n ; :: thesis: ex k being Nat st

( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= p & p < k / (2 |^ n) )

0 in REAL by XREAL_0:def 1;

then reconsider p1 = p as Element of REAL by A1, A2, XXREAL_0:46;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

set k = [\((p1 * (2 |^ n)) + 1)/];

A3: ((p1 * (2 |^ n)) + 1) - 1 = p1 * (2 |^ n) ;

then A4: 0 < [\((p1 * (2 |^ n)) + 1)/] by A1, INT_1:def 6;

then reconsider k = [\((p1 * (2 |^ n)) + 1)/] as Element of NAT by INT_1:3;

A5: p1 * (2 |^ n) < k by A3, INT_1:def 6;

A6: 0 < 2 |^ n by PREPOWER:6;

A7: now :: thesis: not k > (2 |^ n) * n

take
k
; :: thesis: ( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= p & p < k / (2 |^ n) )
p1 * (2 |^ n) < (2 |^ n) * n
by A2, A6, XREAL_1:68;

then A8: (p1 * (2 |^ n)) + 1 < ((2 |^ n) * n) + 1 by XREAL_1:6;

reconsider N = (2 |^ n) * n as Integer ;

assume A9: k > (2 |^ n) * n ; :: thesis: contradiction

A10: [\N/] = N by INT_1:25;

k <= (p1 * (2 |^ n)) + 1 by INT_1:def 6;

then (2 |^ n) * n < (p1 * (2 |^ n)) + 1 by A9, XXREAL_0:2;

hence contradiction by A9, A8, A10, INT_1:67; :: thesis: verum

end;then A8: (p1 * (2 |^ n)) + 1 < ((2 |^ n) * n) + 1 by XREAL_1:6;

reconsider N = (2 |^ n) * n as Integer ;

assume A9: k > (2 |^ n) * n ; :: thesis: contradiction

A10: [\N/] = N by INT_1:25;

k <= (p1 * (2 |^ n)) + 1 by INT_1:def 6;

then (2 |^ n) * n < (p1 * (2 |^ n)) + 1 by A9, XXREAL_0:2;

hence contradiction by A9, A8, A10, INT_1:67; :: thesis: verum

k <= (p1 * (2 |^ n)) + 1 by INT_1:def 6;

then A11: k - 1 <= p1 * (2 |^ n) by XREAL_1:20;

0 + 1 <= k by A4, NAT_1:13;

hence ( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= p & p < k / (2 |^ n) ) by A6, A7, A5, A11, XREAL_1:79, XREAL_1:81; :: thesis: verum