let i, n, k, u be Nat; ( u > n |^ k & n >= k & k > i implies (n choose i) * (u |^ i) < (u |^ k) / n )
assume A1:
( u > n |^ k & n >= k & k > i )
; (n choose i) * (u |^ i) < (u |^ k) / n
then A2:
k >= i + 1
by NAT_1:13;
A3:
u >= 1
by A1, NAT_1:14;
A4:
n > 0
by A1;
then
n >= 1
by NAT_1:14;
then
n |^ (i + 1) <= n |^ k
by A2, PREPOWER:93;
then
n |^ (i + 1) < u
by A1, XXREAL_0:2;
then A5:
(n |^ (i + 1)) * (u |^ i) < u * (u |^ i)
by XREAL_1:68;
u * (u |^ i) = u |^ (i + 1)
by NEWTON:6;
then
u * (u |^ i) <= u |^ k
by A3, A2, PREPOWER:93;
then
( (n |^ (i + 1)) * (u |^ i) < u |^ k & n |^ (i + 1) = n * (n |^ i) )
by A5, XXREAL_0:2, NEWTON:6;
then
n * ((n |^ i) * (u |^ i)) < u |^ k
;
then A6:
(n |^ i) * (u |^ i) < (u |^ k) / n
by A4, XREAL_1:81;
i <= n
by A1, XXREAL_0:2;
then
n choose i <= n |^ i
by Th13;
then
(n choose i) * (u |^ i) <= (n |^ i) * (u |^ i)
by XREAL_1:64;
hence
(n choose i) * (u |^ i) < (u |^ k) / n
by A6, XXREAL_0:2; verum