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 ; :: 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 ; :: 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
.= (((n2 !) / (n2 !)) * ((n - 1) * n)) / 2 by
.= ((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 ; :: 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 ;
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 ;
then A8: n choose 2 = ((n2 !) * (n1 * n)) / ((n2 !) * (2 !)) by
.= (((n2 !) / (n2 !)) * (n1 * n)) / 2 by
.= (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
.= (((n3 !) / (n3 !)) * ((n2 * n1) * n)) / 6 by
.= ((n * n1) * n2) / 6 by A11 ;
n >= 3 + 1 by ;
then n choose 4 = ((n4 !) * (((n3 * n2) * n1) * n)) / ((n4 !) * (4 !)) by
.= (((n4 !) / (n4 !)) * (((n3 * n2) * n1) * n)) / 24 by
.= (((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 ; :: 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