I have a truly marvellous proof of this proposition, but I can't get TeX working on my iPad.
OK, you asked for it !
We need to start by defining a function f(m,n) of 2 integers, m and n where n is used as before and m is the degree:
f(0,n) = n { = sum_{i=1}^{i=n} 1 } : for n > 0
f(m,n) = f(m-1,1) + f(m-1,2) + ... + f(m-1,n) : for n > 0, m > 0 I shall refer to this statement as (X)
We see that : f(1,n) = 1 + 2 + 3 + ... + n = n(n+1)/2 (we know the formula)
and Reivers query : f(2,n ) = f(1,1) + f(1,2) + ... + f(1,n )
= 1 + 2 + 6 + ... + n(n+1)/2 = n(n+1)(n+2)/6 (AbelianGrape's formula)
So f(m,n) generalises Reiver's query for m > 2. Note also that f(m,1) = f(m-1,1) = ... = f(0,1) = 1.
For some simplicity, let us use C(n,k) to be what is commonly known as the
Binomial coefficient of n indexed by k where n & k are integers. We have the identity:
C(n,k) = n! / ( k! (n-k)! )
We need
Pascal's rule that states C(n,k) = C(n-1,k) + C(n-1,k-1) for n>0, k>0. This formula is "trivial" in so far as you can show it from the formula I gave for C(n,k) in 2 lines but also relate it directly to Pascal's triangle.
I want to demonstrate a formula for f(m,n) in terms of the function C(.,.), using a 2 step
induction argument.
Proposition :
f(m,n) = C(m+n,m+1) for m >= 0, n > 0 I shall refer to this statement as (Y)
OK, so we make the outer inductive statement H(M) which states that formula (Y) is true for all m <= M.
First note 2 things :
1) for m = 0, C(n,1) = n = f(0,n) so (Y) is true for m = 0 for all n > 0
2) for n = 1, C(m+1,m+1) = 1 = f(m,1) so (Y) is true for m = 1 and all m >= 0
1) implies that H(0) is true. So let us assume H is true up to M >= 0 and show that this implies H(M+1) is also true.
Well, for n > 1, (X) can be written alternatively:
f(m,n) = f(m-1,1) + f(m-1,2) + ... + f(m-1,n)
= f(m,n-1) + f(m-1,n) I shall refer to this statement as (Z)
We make an inner inductive statement to induct on n this time. J(M+1,N) states that for m = M+1 fixed, formula (Y) is true for n <= N.
We know from 2) that J(M+1,1) is true for all M, so we want to show that J(M+1,N) implies J(M+1,N+1) for all N >= 1, meaning we want to show f(M+1,N+1) is true under the inner inductive statement that J(M+1,N) is true and also under the outer inductive statement that H(M) is true.
Equation (Z) is in this case :
f(M+1,N+1) = f(M+1,N) + f(M,N+1)
= C(M+1+N,M+2) + C(M+N+1,M+1) by J(M+1,N) and H(M)
= C(M+N+1,M+1) by Pascal's rule
Which is what we want. This shows in the first instance that J(M+1,N+1) is true, so that the inner induction implies formula (X) is true for all n >=1 with m = M+1. And that therefore the outer induction is true for all m >=0.
So, look I know this is laid out in excessive detail, more-so than is needed by most to believe the truth of the formula that srw & I spotted but I'm trying to show that to try to explain the double induction carefully is tedious when the key equality is essentially Pascal's rule that I think is fair enough to say is a trivial identity.