Theorem sticksstones15

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

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

Proof

Step	Hyp	Ref	Expression
1		sticksstones15.1	$$⊢\phi \to N\in {\mathbb{N}}_0$$
2		sticksstones15.2	$$⊢\phi \to K\in {\mathbb{N}}_0$$
3		sticksstones15.3	$$⊢A=\left\{g|\left(g:\left(1\dots K+1\right)⟶{\mathbb{N}}_0\wedge \sum _{i=1}^{K+1}g\left(i\right)=N\right)\right\}$$
4		eqid	$$⊢\left(v\in A⟼\left(z\in \left(1\dots K\right)⟼z+\sum _{t=1}^{z}v\left(t\right)\right)\right)=\left(v\in A⟼\left(z\in \left(1\dots K\right)⟼z+\sum _{t=1}^{z}v\left(t\right)\right)\right)$$
5		eqid	$$⊢\left(u\in \left\{l|\left(l:\left(1\dots K\right)⟶\left(1\dots N+K\right)\wedge \forall x\in \left(1\dots K\right)\forall y\in \left(1\dots K\right)\left(x<y\to l\left(x\right)<l\left(y\right)\right)\right)\right\}⟼if\left(K=0,\left\{⟨1,N⟩\right\},\left(w\in \left(1\dots K+1\right)⟼if\left(w=K+1,N+K-u\left(K\right),if\left(w=1,u\left(1\right)-1,u\left(w\right)-u\left(w-1\right)-1\right)\right)\right)\right)\right)=\left(u\in \left\{l|\left(l:\left(1\dots K\right)⟶\left(1\dots N+K\right)\wedge \forall x\in \left(1\dots K\right)\forall y\in \left(1\dots K\right)\left(x<y\to l\left(x\right)<l\left(y\right)\right)\right)\right\}⟼if\left(K=0,\left\{⟨1,N⟩\right\},\left(w\in \left(1\dots K+1\right)⟼if\left(w=K+1,N+K-u\left(K\right),if\left(w=1,u\left(1\right)-1,u\left(w\right)-u\left(w-1\right)-1\right)\right)\right)\right)\right)$$
6		feq1	$$⊢l=f\to \left(l:\left(1\dots K\right)⟶\left(1\dots N+K\right)\leftrightarrow f:\left(1\dots K\right)⟶\left(1\dots N+K\right)\right)$$
7		fveq1	$$⊢l=f\to l\left(x\right)=f\left(x\right)$$
8		fveq1	$$⊢l=f\to l\left(y\right)=f\left(y\right)$$
9	7 8	breq12d	$$⊢l=f\to \left(l\left(x\right)<l\left(y\right)\leftrightarrow f\left(x\right)<f\left(y\right)\right)$$
10	9	imbi2d	$$⊢l=f\to \left(\left(x<y\to l\left(x\right)<l\left(y\right)\right)\leftrightarrow \left(x<y\to f\left(x\right)<f\left(y\right)\right)\right)$$
11	10	2ralbidv	$$⊢l=f\to \left(\forall x\in \left(1\dots K\right)\forall y\in \left(1\dots K\right)\left(x<y\to l\left(x\right)<l\left(y\right)\right)\leftrightarrow \forall x\in \left(1\dots K\right)\forall y\in \left(1\dots K\right)\left(x<y\to f\left(x\right)<f\left(y\right)\right)\right)$$
12	6 11	anbi12d	$$⊢l=f\to \left(\left(l:\left(1\dots K\right)⟶\left(1\dots N+K\right)\wedge \forall x\in \left(1\dots K\right)\forall y\in \left(1\dots K\right)\left(x<y\to l\left(x\right)<l\left(y\right)\right)\right)\leftrightarrow \left(f:\left(1\dots K\right)⟶\left(1\dots N+K\right)\wedge \forall x\in \left(1\dots K\right)\forall y\in \left(1\dots K\right)\left(x<y\to f\left(x\right)<f\left(y\right)\right)\right)\right)$$
13	12	cbvabv	$$⊢\left\{l|\left(l:\left(1\dots K\right)⟶\left(1\dots N+K\right)\wedge \forall x\in \left(1\dots K\right)\forall y\in \left(1\dots K\right)\left(x<y\to l\left(x\right)<l\left(y\right)\right)\right)\right\}=\left\{f|\left(f:\left(1\dots K\right)⟶\left(1\dots N+K\right)\wedge \forall x\in \left(1\dots K\right)\forall y\in \left(1\dots K\right)\left(x<y\to f\left(x\right)<f\left(y\right)\right)\right)\right\}$$
14	1 2 4 5 3 13	sticksstones14	$$⊢\phi \to \left|A\right|=\left(\genfrac{}{}{0ex}{}{N+K}{K}\right)$$