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

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A3: S₁[m] ; :: thesis: S₁[m + 1]
set m1 = m + 1;
assume A4: (m + 1) ^2 <= n ; :: thesis: ex T being _Theta st n choose (m + 1) = ((n |^ (m + 1)) / ((m + 1) !)) * (1 + (T * (((m + 1) ^2) / n)))
m <= m + 1 by NAT_1:11;
then A5: ( m ^2 = m * m & m * m <= (m + 1) * (m + 1) & (m + 1) * (m + 1) = (m + 1) ^2 ) by XREAL_1:66, SQUARE_1:def 1;
then consider T being _Theta such that
A6: n choose m = ((n |^ m) / (m !)) * (1 + (T * ((m ^2) / n))) by A3, A4, XXREAL_0:2;
A7: ((n - m) / (m + 1)) * 1 = ((n - m) / (m + 1)) * (n / n) by A5, A4, XCMPLX_1:60
.= ((n - m) * n) / ((m + 1) * n) by XCMPLX_1:76
.= ((n - m) / n) * (n / (m + 1)) by XCMPLX_1:76 ;
m ^2 <= n by A5, A4, XXREAL_0:2;
then A8: ( (m ^2) / n <= n / n & n / n = 1 ) by A5, A4, XREAL_1:72, XCMPLX_1:60;
reconsider I = 1 as _Theta by Def1;
(n - m) / n = (n / n) - (m / n) by XCMPLX_1:120
.= 1 - (1 * (m / n)) by A5, A4, XCMPLX_1:60 ;
then (1 + (T * ((m ^2) / n))) * ((n - m) / n) = (1 + (T * ((m ^2) / n))) * (1 + ((- I) * (m / n))) ;
then consider t being _Theta such that
A9: (1 + (T * ((m ^2) / n))) * ((n - m) / n) = 1 + (t * (((m ^2) / n) + (2 * (m / n)))) by A8, Th3;
( (m + 1) ^2 = (m + 1) * (m + 1) & (m + 1) * (m + 1) = ((m * m) + (2 * m)) + 1 & m * m = m ^2 ) by SQUARE_1:def 1;
then ((m ^2) + (2 * m)) + 0 <= (m + 1) ^2 by XREAL_1:7;
then ((m ^2) + (2 * m)) / n <= ((m + 1) ^2) / n by XREAL_1:72;
then ((m ^2) / n) + ((2 * m) / n) <= ((m + 1) ^2) / n by XCMPLX_1:62;
then |.(((m ^2) / n) + (2 * (m / n))).| <= |.(((m + 1) ^2) / n).| by XCMPLX_1:74;
then consider s being _Theta such that
A10: t * (((m ^2) / n) + (2 * (m / n))) = s * (((m + 1) ^2) / n) by Th2;
( (m + 1) * (m !) = (m + 1) ! & n * (n |^ m) = n |^ (m + 1) ) by NEWTON:6, NEWTON:15;
then A11: (n / (m + 1)) * ((n |^ m) / (m !)) = (n |^ (m + 1)) / ((m + 1) !) by XCMPLX_1:76;
n choose (m + 1) = ((n - m) / (m + 1)) * (n choose m) by IRRAT_1:5
.= ((n |^ (m + 1)) / ((m + 1) !)) * (((n - m) / n) * (1 + (T * ((m ^2) / n)))) by A11, A6, A7
.= ((n |^ (m + 1)) / ((m + 1) !)) * (1 + (s * (((m + 1) ^2) / n))) by A10, A9 ;
hence ex T being _Theta st n choose (m + 1) = ((n |^ (m + 1)) / ((m + 1) !)) * (1 + (T * (((m + 1) ^2) / n))) ; :: thesis: verum

end;

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