let j, n, k be Nat; :: thesis: ( k < n implies 1 - ((j * k) / n) <= (1 - (k / n)) |^ j )
assume A1: k < n ; :: thesis: 1 - ((j * k) / n) <= (1 - (k / n)) |^ j
defpred S₁[ Nat] means 1 - (($1 * k) / n) <= (1 - (k / n)) |^ $1;
A2: S₁[ 0 ] by NEWTON:4;
A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
set i1 = i + 1;
( n / n > k / n & n / n = 1 ) by A1, XCMPLX_1:60, XREAL_1:74;
then A4: 1 - (k / n) >= 0 by XREAL_1:50;
assume S₁[i] ; :: thesis: S₁[i + 1]
then A5: (1 - ((i * k) / n)) * (1 - (k / n)) <= ((1 - (k / n)) |^ i) * (1 - (k / n)) by A4, XREAL_1:64;
A6: (1 - ((i * k) / n)) - (k / n) = 1 - (((i * k) / n) + (k / n))
.= 1 - (((i * k) + k) / n) by XCMPLX_1:62
.= 1 - (((i + 1) * k) / n) ;
(1 - ((i * k) / n)) * (1 - (k / n)) = ((1 - ((i * k) / n)) - (k / n)) + (((i * k) / n) * (k / n)) ;
then (1 - ((i * k) / n)) * (1 - (k / n)) >= ((1 - ((i * k) / n)) - (k / n)) + 0 by XREAL_1:7;
then 1 - (((i + 1) * k) / n) <= ((1 - (k / n)) |^ i) * (1 - (k / n)) by A6, A5, XXREAL_0:2;
hence S₁[i + 1] by NEWTON:6; :: thesis: verum

end;

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