let n be Element of 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;
n2 ! <> 0 by NEWTON:23;
then A2: (n2 ! ) / (n2 ! ) = 1 by XCMPLX_1:60;
( (n1 + 1) ! = (n1 ! ) * n & (n2 + 1) ! = (n2 ! ) * (n2 + 1) ) by NEWTON:21;
then n choose 2 = ((n2 ! ) * ((n - 1) * n)) / ((n2 ! ) * (2 ! )) by A1, NEWTON:def 3
.= (((n2 ! ) / (n2 ! )) * ((n - 1) * n)) / 2 by NEWTON:20, XCMPLX_1:84
.= ((n - 1) * n) / 2 by A2 ;
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 A3: 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 > 1 & n > 2 & n > 3 & n >= 3 + 1 ) by NAT_1:13, XXREAL_0:2;
then reconsider n1 = n - 1, n2 = n - 2, n3 = n - 3, n4 = n - 4 as Element of NAT by NAT_1:21;
( n2 ! <> 0 & n3 ! <> 0 & n4 ! <> 0 ) by NEWTON:23;
then A4: ( (n2 ! ) / (n2 ! ) = 1 & (n3 ! ) / (n3 ! ) = 1 & (n4 ! ) / (n4 ! ) = 1 ) by XCMPLX_1:60;
A5: ( (n1 + 1) ! = (n1 ! ) * n & (n2 + 1) ! = (n2 ! ) * (n2 + 1) & (n3 + 1) ! = (n3 ! ) * (n3 + 1) & (n4 + 1) ! = (n4 ! ) * (n4 + 1) ) by NEWTON:21;
n >= 2 by A3, XXREAL_0:2;
then A6: n choose 2 = ((n2 ! ) * (n1 * n)) / ((n2 ! ) * (2 ! )) by A5, NEWTON:def 3
.= (((n2 ! ) / (n2 ! )) * (n1 * n)) / 2 by NEWTON:20, XCMPLX_1:84
.= (n * n1) / 2 by A4 ;
A7: n choose 3 = ((n3 ! ) * ((n2 * n1) * n)) / ((n3 ! ) * (3 ! )) by A3, A5, NEWTON:def 3
.= (((n3 ! ) / (n3 ! )) * ((n2 * n1) * n)) / 6 by Th60, XCMPLX_1:84
.= ((n * n1) * n2) / 6 by A4 ;
n >= 3 + 1 by A3, NAT_1:13;
then n choose 4 = ((n4 ! ) * (((n3 * n2) * n1) * n)) / ((n4 ! ) * (4 ! )) by A5, NEWTON:def 3
.= (((n4 ! ) / (n4 ! )) * (((n3 * n2) * n1) * n)) / 24 by Th60, XCMPLX_1:84
.= (((n * n1) * n2) * n3) / 24 by A4 ;
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 A3, A6, A7, 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