sticksstones16

Description: Sticks and stones with collapsed definitions for positive integers. (Contributed by metakunt, 20-Oct-2024)

	Ref	Expression
Hypotheses	sticksstones16.1	$⊢ φ \to N \in ℕ_{0}$
	sticksstones16.2	$⊢ φ \to K \in ℕ$
	sticksstones16.3	$⊢ A = \{g \| (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} g (i) = N)\}$
Assertion	sticksstones16	$⊢ φ \to \|A\| = (\binom{N + K - 1}{K - 1})$

Proof

Step	Hyp	Ref	Expression
1		sticksstones16.1	$⊢ φ \to N \in ℕ_{0}$
2		sticksstones16.2	$⊢ φ \to K \in ℕ$
3		sticksstones16.3	$⊢ A = \{g \| (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} g (i) = N)\}$
4		fveq2	$⊢ i = j \to g (i) = g (j)$
5	4	cbvsumv	$⊢ \sum_{i = 1}^{K} g (i) = \sum_{j = 1}^{K} g (j)$
6	5	eqeq1i	$⊢ \sum_{i = 1}^{K} g (i) = N \leftrightarrow \sum_{j = 1}^{K} g (j) = N$
7	6	anbi2i	$⊢ (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} g (i) = N) \leftrightarrow (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{j = 1}^{K} g (j) = N)$
8	7	abbii	$⊢ \{g \| (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{i = 1}^{K} g (i) = N)\} = \{g \| (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{j = 1}^{K} g (j) = N)\}$
9	3 8	eqtri	$⊢ A = \{g \| (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{j = 1}^{K} g (j) = N)\}$
10	9	a1i	$⊢ φ \to A = \{g \| (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{j = 1}^{K} g (j) = N)\}$
11		nfv	$⊢ Ⅎ g φ$
12	2	nncnd	$⊢ φ \to K \in ℂ$
13		1cnd	$⊢ φ \to 1 \in ℂ$
14	12 13	npcand	$⊢ φ \to K - 1 + 1 = K$
15	14	eqcomd	$⊢ φ \to K = K - 1 + 1$
16	15	oveq2d	$⊢ φ \to (1 \dots K) = (1 \dots K - 1 + 1)$
17	16	feq2d	$⊢ φ \to (g : (1 \dots K) ⟶ ℕ_{0} \leftrightarrow g : (1 \dots K - 1 + 1) ⟶ ℕ_{0})$
18	16	sumeq1d	$⊢ φ \to \sum_{j = 1}^{K} g (j) = \sum_{j = 1}^{K - 1 + 1} g (j)$
19	18	eqeq1d	$⊢ φ \to (\sum_{j = 1}^{K} g (j) = N \leftrightarrow \sum_{j = 1}^{K - 1 + 1} g (j) = N)$
20	17 19	anbi12d	$⊢ φ \to ((g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{j = 1}^{K} g (j) = N) \leftrightarrow (g : (1 \dots K - 1 + 1) ⟶ ℕ_{0} \land \sum_{j = 1}^{K - 1 + 1} g (j) = N))$
21	11 20	abbid	$⊢ φ \to \{g \| (g : (1 \dots K) ⟶ ℕ_{0} \land \sum_{j = 1}^{K} g (j) = N)\} = \{g \| (g : (1 \dots K - 1 + 1) ⟶ ℕ_{0} \land \sum_{j = 1}^{K - 1 + 1} g (j) = N)\}$
22	10 21	eqtrd	$⊢ φ \to A = \{g \| (g : (1 \dots K - 1 + 1) ⟶ ℕ_{0} \land \sum_{j = 1}^{K - 1 + 1} g (j) = N)\}$
23	22	fveq2d	$⊢ φ \to \|A\| = \|\{g \| (g : (1 \dots K - 1 + 1) ⟶ ℕ_{0} \land \sum_{j = 1}^{K - 1 + 1} g (j) = N)\}\|$
24		nnm1nn0	$⊢ K \in ℕ \to K - 1 \in ℕ_{0}$
25	2 24	syl	$⊢ φ \to K - 1 \in ℕ_{0}$
26		fveq2	$⊢ j = i \to g (j) = g (i)$
27	26	cbvsumv	$⊢ \sum_{j = 1}^{K - 1 + 1} g (j) = \sum_{i = 1}^{K - 1 + 1} g (i)$
28	27	eqeq1i	$⊢ \sum_{j = 1}^{K - 1 + 1} g (j) = N \leftrightarrow \sum_{i = 1}^{K - 1 + 1} g (i) = N$
29	28	anbi2i	$⊢ (g : (1 \dots K - 1 + 1) ⟶ ℕ_{0} \land \sum_{j = 1}^{K - 1 + 1} g (j) = N) \leftrightarrow (g : (1 \dots K - 1 + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K - 1 + 1} g (i) = N)$
30	29	abbii	$⊢ \{g \| (g : (1 \dots K - 1 + 1) ⟶ ℕ_{0} \land \sum_{j = 1}^{K - 1 + 1} g (j) = N)\} = \{g \| (g : (1 \dots K - 1 + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K - 1 + 1} g (i) = N)\}$
31	1 25 30	sticksstones15	$⊢ φ \to \|\{g \| (g : (1 \dots K - 1 + 1) ⟶ ℕ_{0} \land \sum_{j = 1}^{K - 1 + 1} g (j) = N)\}\| = (\binom{N + K - 1}{K - 1})$
32	23 31	eqtrd	$⊢ φ \to \|A\| = (\binom{N + K - 1}{K - 1})$

Metamath Proof Explorer

Theorem sticksstones16

Proof