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) )
assume A1: x = 1 / (n + 1) ; :: thesis: (n ! ) / (((n + k) + 1) ! ) <= x ^ (k + 1)
defpred S₁[ Element of NAT ] means (n ! ) / (((n + $1) + 1) ! ) <= x ^ ($1 + 1);
for k being Element of NAT holds (n ! ) / (((n + k) + 1) ! ) <= x ^ (k + 1)

proof

A2: now

A3: ( n + 1 <> 0 & n ! <> 0 ) by NEWTON:23;
(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 A3, XCMPLX_0:def 7
.= x by A1 ;
hence S₁[ 0 ] by POWER:30; :: thesis: verum

end;

A4: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
n + (k + 1) >= n + 0 by XREAL_1:8;
then (n + (k + 1)) + 1 >= n + 1 by XREAL_1:8;
then 1 / ((n + (k + 1)) + 1) <= 1 / (n + 1) by XREAL_1:87;
then A7: ((n + (k + 1)) + 1) " <= 1 / (n + 1) ;
A8: (x ^ (k + 1)) * x = (x ^ (k + 1)) * (x ^ 1) by POWER:30
.= x ^ ((k + 1) + 1) by A1, POWER:32 ;
(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) " ) ;
hence S₁[k + 1] by A1, A5, A7, A8, XREAL_1:68; :: thesis: verum

end;

thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A4); :: thesis: verum

end;

hence (n ! ) / (((n + k) + 1) ! ) <= x ^ (k + 1) ; :: thesis: verum