let n, k be Element of NAT ; :: thesis: for x being real number st x = 1 / (n + 1) holds
(n ! ) / (((n + k) + 1) ! ) <= x ^ (k + 1)
let x be real number ; :: thesis: ( x = 1 / (n + 1) implies (n ! ) / (((n + k) + 1) ! ) <= x ^ (k + 1) )
defpred S₁[ Element of NAT ] means (n ! ) / (((n + $1) + 1) ! ) <= x ^ ($1 + 1);
A1: n ! <> 0 by NEWTON:23;
assume A2: x = 1 / (n + 1) ; :: thesis: (n ! ) / (((n + k) + 1) ! ) <= x ^ (k + 1)

A3: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
A5: (n ! ) / (((n + (k + 1)) + 1) ! ) = (n ! ) * ((((n + (k + 1)) + 1) ! ) " )
.= (n ! ) * ((((n + (k + 1)) + 1) * (((n + k) + 1) ! )) " ) by NEWTON:21
.= (n ! ) * ((((n + (k + 1)) + 1) " ) * ((((n + k) + 1) ! ) " )) by XCMPLX_1:205
.= ((n ! ) * ((((n + k) + 1) ! ) " )) * (((n + (k + 1)) + 1) " )
.= ((n ! ) / (((n + k) + 1) ! )) * (((n + (k + 1)) + 1) " ) ;
n + (k + 1) >= n + 0 by XREAL_1:8;
then (n + (k + 1)) + 1 >= n + 1 by XREAL_1:8;
then A6: ((n + (k + 1)) + 1) " <= 1 / (n + 1) by XREAL_1:87;
(x ^ (k + 1)) * x = (x ^ (k + 1)) * (x ^ 1) by POWER:30
.= x ^ ((k + 1) + 1) by A2, POWER:32 ;
hence S₁[k + 1] by A2, A4, A6, A5, XREAL_1:68; :: thesis: verum

end;

(n ! ) / ((n + 1) ! ) = (n ! ) / ((n + 1) * (n ! )) by NEWTON:21
.= (n ! ) * (((n + 1) * (n ! )) " )
.= (n ! ) * (((n + 1) " ) * ((n ! ) " )) by XCMPLX_1:205
.= ((n ! ) * ((n ! ) " )) * ((n + 1) " )
.= 1 * ((n + 1) " ) by A1, XCMPLX_0:def 7
.= x by A2 ;
then A7: S₁[ 0 ] by POWER:30;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A7, A3);
hence (n ! ) / (((n + k) + 1) ! ) <= x ^ (k + 1) ; :: thesis: verum