let n, k be Nat; :: thesis: ( k <= n implies n choose k <= n |^ k )

defpred S_{1}[ Nat] means ( $1 <= n implies n choose $1 <= n |^ $1 );

n choose 0 = 1 by NEWTON:19;

then A1: S_{1}[ 0 ]
by NEWTON:4;

A2: for m being Nat st S_{1}[m] holds

S_{1}[m + 1]
_{1}[m]
from NAT_1:sch 2(A1, A2);

hence ( k <= n implies n choose k <= n |^ k ) ; :: thesis: verum

defpred S

n choose 0 = 1 by NEWTON:19;

then A1: S

A2: for m being Nat st S

S

proof

for m being Nat holds S
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A3: S_{1}[m]
; :: thesis: S_{1}[m + 1]

set m1 = m + 1;

assume A4: m + 1 <= n ; :: thesis: n choose (m + 1) <= n |^ (m + 1)

then m < n by NAT_1:13;

then A5: n - m > m - m by XREAL_1:14;

A6: n - m <= n - 0 by XREAL_1:10;

A7: n choose (m + 1) = ((n - m) / (m + 1)) * (n choose m) by IRRAT_1:5;

(n - m) / (m + 1) <= (n - m) / 1 by A5, XREAL_1:118, NAT_1:11;

then (n - m) / (m + 1) <= n by A6, XXREAL_0:2;

then A8: n choose (m + 1) <= n * (n choose m) by A7, XREAL_1:64;

n * (n choose m) <= n * (n |^ m) by A3, A4, NAT_1:13, XREAL_1:64;

then n choose (m + 1) <= n * (n |^ m) by A8, XXREAL_0:2;

hence n choose (m + 1) <= n |^ (m + 1) by NEWTON:6; :: thesis: verum

end;assume A3: S

set m1 = m + 1;

assume A4: m + 1 <= n ; :: thesis: n choose (m + 1) <= n |^ (m + 1)

then m < n by NAT_1:13;

then A5: n - m > m - m by XREAL_1:14;

A6: n - m <= n - 0 by XREAL_1:10;

A7: n choose (m + 1) = ((n - m) / (m + 1)) * (n choose m) by IRRAT_1:5;

(n - m) / (m + 1) <= (n - m) / 1 by A5, XREAL_1:118, NAT_1:11;

then (n - m) / (m + 1) <= n by A6, XXREAL_0:2;

then A8: n choose (m + 1) <= n * (n choose m) by A7, XREAL_1:64;

n * (n choose m) <= n * (n |^ m) by A3, A4, NAT_1:13, XREAL_1:64;

then n choose (m + 1) <= n * (n |^ m) by A8, XXREAL_0:2;

hence n choose (m + 1) <= n |^ (m + 1) by NEWTON:6; :: thesis: verum

hence ( k <= n implies n choose k <= n |^ k ) ; :: thesis: verum