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 :: 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 )

( not not n = 0 & ... & not n = 3 or 3 < n ) ;

per cases then ( n = 0 or n = 1 or n = 2 or n = 3 or n > 3 ) ;

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:21, 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:21, NEWTON:23, 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:15;
A3: (n2 !) / (n2 !) = 1 by XCMPLX_1:60;
(n1 + 1) ! = (n1 !) * n by NEWTON:15;
then n choose 2 = ((n2 !) * ((n - 1) * n)) / ((n2 !) * (2 !)) by A1, A2, NEWTON:def 3
.= (((n2 !) / (n2 !)) * ((n - 1) * n)) / 2 by NEWTON:14, XCMPLX_1:83
.= ((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:21, NEWTON:23, 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:15;
A6: (n2 + 1) ! = (n2 !) * (n2 + 1) by NEWTON:15;
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:14, XCMPLX_1:83
.= (n * n1) / 2 by A7 ;
A9: (n4 !) / (n4 !) = 1 by XCMPLX_1:60;
A10: (n4 + 1) ! = (n4 !) * (n4 + 1) by NEWTON:15;
A11: (n3 !) / (n3 !) = 1 by XCMPLX_1:60;
A12: (n3 + 1) ! = (n3 !) * (n3 + 1) by NEWTON:15;
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 Th50, XCMPLX_1:83
.= ((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 Th50, XCMPLX_1:83
.= (((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:23, 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