let n, k be Nat; :: thesis: for p being R_eal st 1 <= k & k <= (2 |^ n) * n & n <= p & (k - 1) / (2 |^ n) <= p holds
k / (2 |^ n) <= p
let p be R_eal; :: thesis: ( 1 <= k & k <= (2 |^ n) * n & n <= p & (k - 1) / (2 |^ n) <= p implies k / (2 |^ n) <= p )
assume A1: ( 1 <= k & k <= (2 |^ n) * n & n <= p & (k - 1) / (2 |^ n) <= p ) ; :: thesis: k / (2 |^ n) <= p
assume p < k / (2 |^ n) ; :: thesis: contradiction
then n < k / (2 |^ n) by A1, XXREAL_0:2;
hence contradiction by A1, PREPOWER:13, XREAL_1:81; :: thesis: verum