A trivial combinatorics result I found, is my proof correct?

Question

I have just finished highschool and have started learning on my own some combinatorics and how to do proofs, and while messing around with sums and Pascal's triangle I found an interesting yet trivial property that I tried to prove. I'm assuming that it has already been found, but I couldn't find anything mentioning it.
So my questions are: Is my proof correct? Has this property been found already? What can this property be used for?

Let $$f(x,n)= \sum_{i_1=1}^n \sum_{i_2=1}^{i_1} \sum_{i_3=1}^{i_2} \cdots \sum_{i_x=1}^{i_{x-1}}i_x \ $$ where $x$ is the number of sigma sums.

My conjecture is that $$f(x,n)={n+x \choose x+1}$$

Proof by induction

Basis step:
$$\begin{align} f(1,n) &=\sum_{i=1}^ni\\ &=\frac{n(n+1)}{2}\\ &={n+1 \choose 2} \end{align}$$ The basis step works. This first result is already proven for all n.

Inductive step: Assume that $f(x,n)= {n+x \choose x+1} $

Now, $$\begin{align}f(x+1,n) &=\sum_{m=1}^n \sum_{i_1=1}^{m} \sum_{i_2=1}^{i_1} \cdots \sum_{i_x=1}^{i_{x-1}}i_x\\ &=\sum_{m=1}^n f(x,m)\\ &=\sum_{m=1}^n {m+x \choose x+1}\\ &=\sum_{l=0}^{n-1}{l+1+x \choose x+1}\\ &={n+x+1 \choose x+2}\\ \end{align}$$ Therefore, if $f(x,n)$ holds, then $f(x+1,n)$ holds.
What I am not sure about is whether I have to use induction to prove that this property holds for every integer $n$ as well,

Answer 1

The proof is correct since you can treat $n$ as fixed. You don't have to induct on $n$ since your base case holds for all $n$. If your base case had been $x=n=0$, then yes, you would have to induct on $n$ as well.

However, there is also a simpler way to prove this identity. First, let's rewrite it slightly:

$$f(x, n) = \sum_{i_1=1}^n \sum_{i_2=1}^{i_1} \sum_{i_3=1}^{i_2} \cdots \sum_{i_x=1}^{i_{x-1}} \sum_{i_{x+1}=1}^{i_x}1$$

Now, notice that this counts the number of ways to choose $i_1, i_2, \ldots, i_{x+1}$ such that $1 \le i_{x+1} \le i_x \le \ldots \le i_1 \le n$. But by Stars and Bars (also known as multichoose), this is just $\binom{n+x}{x+1}$ as desired.