let n, k be Nat; :: thesis: ( k <= n implies n ! <= (k !) * (n |^ (n -' k)) )
assume A1: k <= n ; :: thesis: n ! <= (k !) * (n |^ (n -' k))
then reconsider nk = n - k as Nat by NAT_1:21;
defpred S1[ Nat] means (k + \$1) ! <= (k !) * ((k + \$1) |^ \$1);
(k + 0) |^ 0 = 1 by NEWTON:4;
then A2: S1[ 0 ] ;
A3: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
set ki1 = (k + i) + 1;
assume A4: S1[i] ; :: thesis: S1[i + 1]
A5: ( (k + i) |^ 0 = 1 & ((k + i) + 1) |^ 0 = 1 ) by NEWTON:4;
A6: (((k + i) + 1) |^ i) * ((k + i) + 1) = ((k + i) + 1) |^ (i + 1) by NEWTON:6;
( k + i < (k + i) + 1 & ( i >= 1 or i = 0 ) ) by ;
then (k + i) |^ i <= ((k + i) + 1) |^ i by ;
then (k !) * ((k + i) |^ i) <= (k !) * (((k + i) + 1) |^ i) by XREAL_1:66;
then A7: (k + i) ! <= (k !) * (((k + i) + 1) |^ i) by ;
((k + i) + 1) ! = ((k + i) !) * ((k + i) + 1) by NEWTON:15;
then ((k + i) + 1) ! <= ((k !) * (((k + i) + 1) |^ i)) * ((k + i) + 1) by ;
hence S1[i + 1] by A6; :: thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch 2(A2, A3);
then S1[nk] ;
hence
n ! <= (k !) * (n |^ (n -' k)) by ; :: thesis: verum