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

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