let n be Nat; :: thesis: ( n choose 1 = n & n choose 2 = (n * (n - 1)) / 2 & n choose 3 = ((n * (n - 1)) * (n - 2)) / 6 & n choose 4 = (((n * (n - 1)) * (n - 2)) * (n - 3)) / 24 )

now

per cases ( n = 0 or n = 1 or n = 2 or n = 3 or n > 3 ) by NAT_1:28;

suppose n = 0 ; :: thesis: ( n choose 1 = n & n choose 2 = (n * (n - 1)) / 2 & n choose 3 = ((n * (n - 1)) * (n - 2)) / 6 & n choose 4 = (((n * (n - 1)) * (n - 2)) * (n - 3)) / 24 )

hence ( n choose 1 = n & n choose 2 = (n * (n - 1)) / 2 & n choose 3 = ((n * (n - 1)) * (n - 2)) / 6 & n choose 4 = (((n * (n - 1)) * (n - 2)) * (n - 3)) / 24 ) by NEWTON:def 3; :: thesis: verum

end;

suppose n = 1 ; :: thesis: ( n choose 1 = n & n choose 2 = (n * (n - 1)) / 2 & n choose 3 = ((n * (n - 1)) * (n - 2)) / 6 & n choose 4 = (((n * (n - 1)) * (n - 2)) * (n - 3)) / 24 )

hence ( n choose 1 = n & n choose 2 = (n * (n - 1)) / 2 & n choose 3 = ((n * (n - 1)) * (n - 2)) / 6 & n choose 4 = (((n * (n - 1)) * (n - 2)) * (n - 3)) / 24 ) by NEWTON:31, NEWTON:def 3; :: thesis: verum

end;

suppose n = 2 ; :: thesis: ( n choose 1 = n & n choose 2 = (n * (n - 1)) / 2 & n choose 3 = ((n * (n - 1)) * (n - 2)) / 6 & n choose 4 = (((n * (n - 1)) * (n - 2)) * (n - 3)) / 24 )

hence ( n choose 1 = n & n choose 2 = (n * (n - 1)) / 2 & n choose 3 = ((n * (n - 1)) * (n - 2)) / 6 & n choose 4 = (((n * (n - 1)) * (n - 2)) * (n - 3)) / 24 ) by NEWTON:31, NEWTON:33, NEWTON:def 3; :: thesis: verum

end;

suppose A1: n = 3 ; :: thesis: ( n choose 1 = n & n choose 2 = (n * (n - 1)) / 2 & n choose 3 = ((n * (n - 1)) * (n - 2)) / 6 & n choose 4 = (((n * (n - 1)) * (n - 2)) * (n - 3)) / 24 )

then reconsider n1 = n - 1, n2 = n - 2 as Element of NAT by NAT_1:20;
A2: (n2 + 1) ! = (n2 ! ) * (n2 + 1) by NEWTON:21;
n2 ! <> 0 by NEWTON:23;
then A3: (n2 ! ) / (n2 ! ) = 1 by XCMPLX_1:60;
(n1 + 1) ! = (n1 ! ) * n by NEWTON:21;
then n choose 2 = ((n2 ! ) * ((n - 1) * n)) / ((n2 ! ) * (2 ! )) by A1, A2, NEWTON:def 3
.= (((n2 ! ) / (n2 ! )) * ((n - 1) * n)) / 2 by NEWTON:20, XCMPLX_1:84
.= ((n - 1) * n) / 2 by A3 ;
hence ( n choose 1 = n & n choose 2 = (n * (n - 1)) / 2 & n choose 3 = ((n * (n - 1)) * (n - 2)) / 6 & n choose 4 = (((n * (n - 1)) * (n - 2)) * (n - 3)) / 24 ) by A1, NEWTON:31, NEWTON:33, NEWTON:def 3; :: thesis: verum

end;

suppose A4: n > 3 ; :: thesis: ( n choose 1 = n & n choose 2 = (n * (n - 1)) / 2 & n choose 3 = ((n * (n - 1)) * (n - 2)) / 6 & n choose 4 = (((n * (n - 1)) * (n - 2)) * (n - 3)) / 24 )

then n >= 3 + 1 by NAT_1:13;
then reconsider n1 = n - 1, n2 = n - 2, n3 = n - 3, n4 = n - 4 as Element of NAT by NAT_1:21, XXREAL_0:2;
A5: (n1 + 1) ! = (n1 ! ) * n by NEWTON:21;
A6: (n2 + 1) ! = (n2 ! ) * (n2 + 1) by NEWTON:21;
n2 ! <> 0 by NEWTON:23;
then A7: (n2 ! ) / (n2 ! ) = 1 by XCMPLX_1:60;
n >= 2 by A4, XXREAL_0:2;
then A8: n choose 2 = ((n2 ! ) * (n1 * n)) / ((n2 ! ) * (2 ! )) by A5, A6, NEWTON:def 3
.= (((n2 ! ) / (n2 ! )) * (n1 * n)) / 2 by NEWTON:20, XCMPLX_1:84
.= (n * n1) / 2 by A7 ;
n4 ! <> 0 by NEWTON:23;
then A9: (n4 ! ) / (n4 ! ) = 1 by XCMPLX_1:60;
A10: (n4 + 1) ! = (n4 ! ) * (n4 + 1) by NEWTON:21;
n3 ! <> 0 by NEWTON:23;
then A11: (n3 ! ) / (n3 ! ) = 1 by XCMPLX_1:60;
A12: (n3 + 1) ! = (n3 ! ) * (n3 + 1) by NEWTON:21;
then A13: n choose 3 = ((n3 ! ) * ((n2 * n1) * n)) / ((n3 ! ) * (3 ! )) by A4, A5, A6, NEWTON:def 3
.= (((n3 ! ) / (n3 ! )) * ((n2 * n1) * n)) / 6 by Th60, XCMPLX_1:84
.= ((n * n1) * n2) / 6 by A11 ;
n >= 3 + 1 by A4, NAT_1:13;
then n choose 4 = ((n4 ! ) * (((n3 * n2) * n1) * n)) / ((n4 ! ) * (4 ! )) by A5, A6, A12, A10, NEWTON:def 3
.= (((n4 ! ) / (n4 ! )) * (((n3 * n2) * n1) * n)) / 24 by Th60, XCMPLX_1:84
.= (((n * n1) * n2) * n3) / 24 by A9 ;
hence ( n choose 1 = n & n choose 2 = (n * (n - 1)) / 2 & n choose 3 = ((n * (n - 1)) * (n - 2)) / 6 & n choose 4 = (((n * (n - 1)) * (n - 2)) * (n - 3)) / 24 ) by A4, A8, A13, NEWTON:33, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence ( n choose 1 = n & n choose 2 = (n * (n - 1)) / 2 & n choose 3 = ((n * (n - 1)) * (n - 2)) / 6 & n choose 4 = (((n * (n - 1)) * (n - 2)) * (n - 3)) / 24 ) ; :: thesis: verum