let n be Nat; :: thesis: for k being Nat st k < n holds
(n |^ k) / (n choose k) <= ((k !) * 1) / ((1 - (k / n)) |^ k)
defpred S₁[ Nat] means ( $1 < n implies (n |^ $1) / (n choose $1) <= (($1 !) * 1) / ((1 - ($1 / n)) |^ $1) );
( n |^ 0 = 1 & n choose 0 = 1 ) by NEWTON:4, NEWTON:19;
then A1: S₁[ 0 ] by NEWTON:12;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
set k1 = k + 1;
assume A4: k + 1 < n ; :: thesis: (n |^ (k + 1)) / (n choose (k + 1)) <= (((k + 1) !) * 1) / ((1 - ((k + 1) / n)) |^ (k + 1))
A5: (n |^ (k + 1)) / (n choose (k + 1)) = (n |^ (k + 1)) / (((n - k) / (k + 1)) * (n choose k)) by IRRAT_1:5
.= ((n |^ (k + 1)) / (n choose k)) / ((n - k) / (k + 1)) by XCMPLX_1:78
.= ((n |^ (k + 1)) / (n choose k)) * ((k + 1) / (n - k)) by XCMPLX_1:79
.= ((n * (n |^ k)) / (n choose k)) * ((k + 1) / (n - k)) by NEWTON:6
.= (((n |^ k) / (n choose k)) * n) * ((k + 1) / (n - k)) by XCMPLX_1:74
.= ((n |^ k) / (n choose k)) * (n * ((k + 1) / (n - k))) ;
k < n by A4, NAT_1:13;
then A6: ( n - k > 0 & n - (k + 1) > 0 ) by XREAL_1:50, A4;
k < k + 1 by NAT_1:13;
then k / n < (k + 1) / n by A4, XREAL_1:74;
then A7: 1 - (k / n) > 1 - ((k + 1) / n) by XREAL_1:10;
A8: 1 - ((k + 1) / n) = (n - (k + 1)) / n by Lm1, A4;
then A9: (1 - (k / n)) |^ (k + 1) > (1 - ((k + 1) / n)) |^ (k + 1) by NAT_1:11, A7, A6, PREPOWER:10;
A10: k < n by A4, NAT_1:13;
A11: (n |^ (k + 1)) / (n choose (k + 1)) <= (((k !) * 1) / ((1 - (k / n)) |^ k)) * (n * ((k + 1) / (n - k))) by A3, A5, XREAL_1:64, A6, A4, NAT_1:13;
A12: (1 / ((1 - (k / n)) |^ k)) * (n / (n - k)) = (1 / ((1 - (k / n)) |^ k)) * (1 / (1 - (k / n))) by A10, Lm1
.= (1 * 1) / (((1 - (k / n)) |^ k) * (1 - (k / n))) by XCMPLX_1:76
.= 1 / ((1 - (k / n)) |^ (k + 1)) by NEWTON:6 ;
A13: (((k !) * 1) / ((1 - (k / n)) |^ k)) * (n * ((k + 1) / (n - k))) = (((k !) * 1) / ((1 - (k / n)) |^ k)) * ((k + 1) * (n / (n - k))) by XCMPLX_1:75
.= ((k !) * (1 / ((1 - (k / n)) |^ k))) * ((k + 1) * (n / (n - k))) by XCMPLX_1:74
.= (((k !) * (k + 1)) * (1 / ((1 - (k / n)) |^ k))) * (n / (n - k))
.= (((k + 1) !) * (1 / ((1 - (k / n)) |^ k))) * (n / (n - k)) by NEWTON:15
.= ((k + 1) !) * (1 / ((1 - (k / n)) |^ (k + 1))) by A12
.= (((k + 1) !) * 1) / ((1 - (k / n)) |^ (k + 1)) by XCMPLX_1:74 ;
(((k + 1) !) * 1) / ((1 - (k / n)) |^ (k + 1)) < (((k + 1) !) * 1) / ((1 - ((k + 1) / n)) |^ (k + 1)) by A8, A6, A4, A9, XREAL_1:76;
hence (n |^ (k + 1)) / (n choose (k + 1)) <= (((k + 1) !) * 1) / ((1 - ((k + 1) / n)) |^ (k + 1)) by A11, A13, XXREAL_0:2; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence for k being Nat st k < n holds
(n |^ k) / (n choose k) <= ((k !) * 1) / ((1 - (k / n)) |^ k) ; :: thesis: verum