let n, k be Nat; :: thesis: for p being ExtReal st k <= (2 |^ n) * n & n <= p holds
k / (2 |^ n) <= p
let p be ExtReal; :: thesis: ( k <= (2 |^ n) * n & n <= p implies k / (2 |^ n) <= p )
assume that
A1: k <= (2 |^ n) * n and
A2: n <= p ; :: thesis: k / (2 |^ n) <= p
assume p < k / (2 |^ n) ; :: thesis: contradiction
then n < k / (2 |^ n) by A2, XXREAL_0:2;
hence contradiction by A1, PREPOWER:6, XREAL_1:79; :: thesis: verum