Theorem sticksstones16

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

	Ref	Expression
Hypotheses	sticksstones16.1	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	sticksstones16.2	$$⊢\phi \to K\in \mathbb{N}$$
	sticksstones16.3	$$⊢A=\left\{g|\left(g:\left(1\dots K\right)⟶{\mathbb{N}}_0\wedge \sum _{i=1}^{K}g\left(i\right)=N\right)\right\}$$
Assertion	sticksstones16	$$⊢\phi \to \left|A\right|=\left(\genfrac{}{}{0ex}{}{N+K-1}{K-1}\right)$$

Proof

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