let n be Nat; 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; ( 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
; 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;
take
k
; ( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= p & p < k / (2 |^ n) )
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; verum