Theorem mccl

Description: A multinomial coefficient, in its standard domain, is a positive integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	mccl.kb	$$⊢\underset{\_}{Ⅎ}kB$$
	mccl.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	mccl.b	$$⊢\phi \to B\in \left({{\mathbb{N}}_0}^A\right)$$
Assertion	mccl	$$⊢\phi \to \frac{\sum _{k\in A}B\left(k\right)!}{\prod _{k\in A}B\left(k\right)!}\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		mccl.kb	$$⊢\underset{\_}{Ⅎ}kB$$
2		mccl.a	$$⊢\phi \to A\in \mathrm{Fin}$$
3		mccl.b	$$⊢\phi \to B\in \left({{\mathbb{N}}_0}^A\right)$$
4		sumeq1	$$⊢a=\varnothing \to \sum _{k\in a}b\left(k\right)=\sum _{k\in \varnothing }b\left(k\right)$$
5	4	fveq2d	$$⊢a=\varnothing \to \sum _{k\in a}b\left(k\right)!=\sum _{k\in \varnothing }b\left(k\right)!$$
6		prodeq1	$$⊢a=\varnothing \to \prod _{k\in a}b\left(k\right)!=\prod _{k\in \varnothing }b\left(k\right)!$$
7	5 6	oveq12d	$$⊢a=\varnothing \to \frac{\sum _{k\in a}b\left(k\right)!}{\prod _{k\in a}b\left(k\right)!}=\frac{\sum _{k\in \varnothing }b\left(k\right)!}{\prod _{k\in \varnothing }b\left(k\right)!}$$
8	7	eleq1d	$$⊢a=\varnothing \to \left(\frac{\sum _{k\in a}b\left(k\right)!}{\prod _{k\in a}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \frac{\sum _{k\in \varnothing }b\left(k\right)!}{\prod _{k\in \varnothing }b\left(k\right)!}\in \mathbb{N}\right)$$
9	8	ralbidv	$$⊢a=\varnothing \to \left(\forall b\in \left({{\mathbb{N}}_0}^a\right)\frac{\sum _{k\in a}b\left(k\right)!}{\prod _{k\in a}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \forall b\in \left({{\mathbb{N}}_0}^a\right)\frac{\sum _{k\in \varnothing }b\left(k\right)!}{\prod _{k\in \varnothing }b\left(k\right)!}\in \mathbb{N}\right)$$
10		oveq2	$$⊢a=\varnothing \to {{\mathbb{N}}_0}^a={{\mathbb{N}}_0}^{\varnothing }$$
11	10	raleqdv	$$⊢a=\varnothing \to \left(\forall b\in \left({{\mathbb{N}}_0}^a\right)\frac{\sum _{k\in \varnothing }b\left(k\right)!}{\prod _{k\in \varnothing }b\left(k\right)!}\in \mathbb{N}\leftrightarrow \forall b\in \left({{\mathbb{N}}_0}^{\varnothing }\right)\frac{\sum _{k\in \varnothing }b\left(k\right)!}{\prod _{k\in \varnothing }b\left(k\right)!}\in \mathbb{N}\right)$$
12	9 11	bitrd	$$⊢a=\varnothing \to \left(\forall b\in \left({{\mathbb{N}}_0}^a\right)\frac{\sum _{k\in a}b\left(k\right)!}{\prod _{k\in a}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \forall b\in \left({{\mathbb{N}}_0}^{\varnothing }\right)\frac{\sum _{k\in \varnothing }b\left(k\right)!}{\prod _{k\in \varnothing }b\left(k\right)!}\in \mathbb{N}\right)$$
13		sumeq1	$$⊢a=c\to \sum _{k\in a}b\left(k\right)=\sum _{k\in c}b\left(k\right)$$
14	13	fveq2d	$$⊢a=c\to \sum _{k\in a}b\left(k\right)!=\sum _{k\in c}b\left(k\right)!$$
15		prodeq1	$$⊢a=c\to \prod _{k\in a}b\left(k\right)!=\prod _{k\in c}b\left(k\right)!$$
16	14 15	oveq12d	$$⊢a=c\to \frac{\sum _{k\in a}b\left(k\right)!}{\prod _{k\in a}b\left(k\right)!}=\frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}$$
17	16	eleq1d	$$⊢a=c\to \left(\frac{\sum _{k\in a}b\left(k\right)!}{\prod _{k\in a}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}\in \mathbb{N}\right)$$
18	17	ralbidv	$$⊢a=c\to \left(\forall b\in \left({{\mathbb{N}}_0}^a\right)\frac{\sum _{k\in a}b\left(k\right)!}{\prod _{k\in a}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \forall b\in \left({{\mathbb{N}}_0}^a\right)\frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}\in \mathbb{N}\right)$$
19		oveq2	$$⊢a=c\to {{\mathbb{N}}_0}^a={{\mathbb{N}}_0}^c$$
20	19	raleqdv	$$⊢a=c\to \left(\forall b\in \left({{\mathbb{N}}_0}^a\right)\frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \forall b\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}\in \mathbb{N}\right)$$
21	18 20	bitrd	$$⊢a=c\to \left(\forall b\in \left({{\mathbb{N}}_0}^a\right)\frac{\sum _{k\in a}b\left(k\right)!}{\prod _{k\in a}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \forall b\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}\in \mathbb{N}\right)$$
22		sumeq1	$$⊢a=c\cup \left\{d\right\}\to \sum _{k\in a}b\left(k\right)=\sum _{k\in c\cup \left\{d\right\}}b\left(k\right)$$
23	22	fveq2d	$$⊢a=c\cup \left\{d\right\}\to \sum _{k\in a}b\left(k\right)!=\sum _{k\in c\cup \left\{d\right\}}b\left(k\right)!$$
24		prodeq1	$$⊢a=c\cup \left\{d\right\}\to \prod _{k\in a}b\left(k\right)!=\prod _{k\in c\cup \left\{d\right\}}b\left(k\right)!$$
25	23 24	oveq12d	$$⊢a=c\cup \left\{d\right\}\to \frac{\sum _{k\in a}b\left(k\right)!}{\prod _{k\in a}b\left(k\right)!}=\frac{\sum _{k\in c\cup \left\{d\right\}}b\left(k\right)!}{\prod _{k\in c\cup \left\{d\right\}}b\left(k\right)!}$$
26	25	eleq1d	$$⊢a=c\cup \left\{d\right\}\to \left(\frac{\sum _{k\in a}b\left(k\right)!}{\prod _{k\in a}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \frac{\sum _{k\in c\cup \left\{d\right\}}b\left(k\right)!}{\prod _{k\in c\cup \left\{d\right\}}b\left(k\right)!}\in \mathbb{N}\right)$$
27	26	ralbidv	$$⊢a=c\cup \left\{d\right\}\to \left(\forall b\in \left({{\mathbb{N}}_0}^a\right)\frac{\sum _{k\in a}b\left(k\right)!}{\prod _{k\in a}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \forall b\in \left({{\mathbb{N}}_0}^a\right)\frac{\sum _{k\in c\cup \left\{d\right\}}b\left(k\right)!}{\prod _{k\in c\cup \left\{d\right\}}b\left(k\right)!}\in \mathbb{N}\right)$$
28		oveq2	$$⊢a=c\cup \left\{d\right\}\to {{\mathbb{N}}_0}^a={{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}$$
29	28	raleqdv	$$⊢a=c\cup \left\{d\right\}\to \left(\forall b\in \left({{\mathbb{N}}_0}^a\right)\frac{\sum _{k\in c\cup \left\{d\right\}}b\left(k\right)!}{\prod _{k\in c\cup \left\{d\right\}}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \forall b\in \left({{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}\right)\frac{\sum _{k\in c\cup \left\{d\right\}}b\left(k\right)!}{\prod _{k\in c\cup \left\{d\right\}}b\left(k\right)!}\in \mathbb{N}\right)$$
30	27 29	bitrd	$$⊢a=c\cup \left\{d\right\}\to \left(\forall b\in \left({{\mathbb{N}}_0}^a\right)\frac{\sum _{k\in a}b\left(k\right)!}{\prod _{k\in a}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \forall b\in \left({{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}\right)\frac{\sum _{k\in c\cup \left\{d\right\}}b\left(k\right)!}{\prod _{k\in c\cup \left\{d\right\}}b\left(k\right)!}\in \mathbb{N}\right)$$
31		sumeq1	$$⊢a=A\to \sum _{k\in a}b\left(k\right)=\sum _{k\in A}b\left(k\right)$$
32	31	fveq2d	$$⊢a=A\to \sum _{k\in a}b\left(k\right)!=\sum _{k\in A}b\left(k\right)!$$
33		prodeq1	$$⊢a=A\to \prod _{k\in a}b\left(k\right)!=\prod _{k\in A}b\left(k\right)!$$
34	32 33	oveq12d	$$⊢a=A\to \frac{\sum _{k\in a}b\left(k\right)!}{\prod _{k\in a}b\left(k\right)!}=\frac{\sum _{k\in A}b\left(k\right)!}{\prod _{k\in A}b\left(k\right)!}$$
35	34	eleq1d	$$⊢a=A\to \left(\frac{\sum _{k\in a}b\left(k\right)!}{\prod _{k\in a}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \frac{\sum _{k\in A}b\left(k\right)!}{\prod _{k\in A}b\left(k\right)!}\in \mathbb{N}\right)$$
36	35	ralbidv	$$⊢a=A\to \left(\forall b\in \left({{\mathbb{N}}_0}^a\right)\frac{\sum _{k\in a}b\left(k\right)!}{\prod _{k\in a}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \forall b\in \left({{\mathbb{N}}_0}^a\right)\frac{\sum _{k\in A}b\left(k\right)!}{\prod _{k\in A}b\left(k\right)!}\in \mathbb{N}\right)$$
37		oveq2	$$⊢a=A\to {{\mathbb{N}}_0}^a={{\mathbb{N}}_0}^A$$
38	37	raleqdv	$$⊢a=A\to \left(\forall b\in \left({{\mathbb{N}}_0}^a\right)\frac{\sum _{k\in A}b\left(k\right)!}{\prod _{k\in A}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \forall b\in \left({{\mathbb{N}}_0}^A\right)\frac{\sum _{k\in A}b\left(k\right)!}{\prod _{k\in A}b\left(k\right)!}\in \mathbb{N}\right)$$
39	36 38	bitrd	$$⊢a=A\to \left(\forall b\in \left({{\mathbb{N}}_0}^a\right)\frac{\sum _{k\in a}b\left(k\right)!}{\prod _{k\in a}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \forall b\in \left({{\mathbb{N}}_0}^A\right)\frac{\sum _{k\in A}b\left(k\right)!}{\prod _{k\in A}b\left(k\right)!}\in \mathbb{N}\right)$$
40		sum0	$$⊢\sum _{k\in \varnothing }b\left(k\right)=0$$
41	40	fveq2i	$$⊢\sum _{k\in \varnothing }b\left(k\right)!=0!$$
42		fac0	$$⊢0!=1$$
43	41 42	eqtri	$$⊢\sum _{k\in \varnothing }b\left(k\right)!=1$$
44		prod0	$$⊢\prod _{k\in \varnothing }b\left(k\right)!=1$$
45	43 44	oveq12i	$$⊢\frac{\sum _{k\in \varnothing }b\left(k\right)!}{\prod _{k\in \varnothing }b\left(k\right)!}=\frac{1}{1}$$
46		1div1e1	$$⊢\frac{1}{1}=1$$
47	45 46	eqtri	$$⊢\frac{\sum _{k\in \varnothing }b\left(k\right)!}{\prod _{k\in \varnothing }b\left(k\right)!}=1$$
48		1nn	$$⊢1\in \mathbb{N}$$
49	47 48	eqeltri	$$⊢\frac{\sum _{k\in \varnothing }b\left(k\right)!}{\prod _{k\in \varnothing }b\left(k\right)!}\in \mathbb{N}$$
50	49	a1i	$$⊢\left(\phi \wedge b\in \left({{\mathbb{N}}_0}^{\varnothing }\right)\right)\to \frac{\sum _{k\in \varnothing }b\left(k\right)!}{\prod _{k\in \varnothing }b\left(k\right)!}\in \mathbb{N}$$
51	50	ralrimiva	$$⊢\phi \to \forall b\in \left({{\mathbb{N}}_0}^{\varnothing }\right)\frac{\sum _{k\in \varnothing }b\left(k\right)!}{\prod _{k\in \varnothing }b\left(k\right)!}\in \mathbb{N}$$
52		nfv	$$⊢Ⅎb\left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)$$
53		nfra1	$$⊢Ⅎb\forall b\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}\in \mathbb{N}$$
54	52 53	nfan	$$⊢Ⅎb\left(\left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)\wedge \forall b\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}\in \mathbb{N}\right)$$
55		simpll	$$⊢\left(\left(\left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)\wedge \forall b\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}\in \mathbb{N}\right)\wedge b\in \left({{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}\right)\right)\to \left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)$$
56		fveq2	$$⊢k=j\to b\left(k\right)=b\left(j\right)$$
57	56	cbvsumv	$$⊢\sum _{k\in c}b\left(k\right)=\sum _{j\in c}b\left(j\right)$$
58	57	a1i	$$⊢b=e\to \sum _{k\in c}b\left(k\right)=\sum _{j\in c}b\left(j\right)$$
59		fveq1	$$⊢b=e\to b\left(j\right)=e\left(j\right)$$
60	59	sumeq2sdv	$$⊢b=e\to \sum _{j\in c}b\left(j\right)=\sum _{j\in c}e\left(j\right)$$
61	58 60	eqtrd	$$⊢b=e\to \sum _{k\in c}b\left(k\right)=\sum _{j\in c}e\left(j\right)$$
62	61	fveq2d	$$⊢b=e\to \sum _{k\in c}b\left(k\right)!=\sum _{j\in c}e\left(j\right)!$$
63		2fveq3	$$⊢k=j\to b\left(k\right)!=b\left(j\right)!$$
64	63	cbvprodv	$$⊢\prod _{k\in c}b\left(k\right)!=\prod _{j\in c}b\left(j\right)!$$
65	64	a1i	$$⊢b=e\to \prod _{k\in c}b\left(k\right)!=\prod _{j\in c}b\left(j\right)!$$
66	59	fveq2d	$$⊢b=e\to b\left(j\right)!=e\left(j\right)!$$
67	66	prodeq2ad	$$⊢b=e\to \prod _{j\in c}b\left(j\right)!=\prod _{j\in c}e\left(j\right)!$$
68	65 67	eqtrd	$$⊢b=e\to \prod _{k\in c}b\left(k\right)!=\prod _{j\in c}e\left(j\right)!$$
69	62 68	oveq12d	$$⊢b=e\to \frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}=\frac{\sum _{j\in c}e\left(j\right)!}{\prod _{j\in c}e\left(j\right)!}$$
70	69	eleq1d	$$⊢b=e\to \left(\frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \frac{\sum _{j\in c}e\left(j\right)!}{\prod _{j\in c}e\left(j\right)!}\in \mathbb{N}\right)$$
71	70	cbvralvw	$$⊢\forall b\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \forall e\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{j\in c}e\left(j\right)!}{\prod _{j\in c}e\left(j\right)!}\in \mathbb{N}$$
72	71	biimpi	$$⊢\forall b\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}\in \mathbb{N}\to \forall e\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{j\in c}e\left(j\right)!}{\prod _{j\in c}e\left(j\right)!}\in \mathbb{N}$$
73	72	ad2antlr	$$⊢\left(\left(\left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)\wedge \forall b\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}\in \mathbb{N}\right)\wedge b\in \left({{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}\right)\right)\to \forall e\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{j\in c}e\left(j\right)!}{\prod _{j\in c}e\left(j\right)!}\in \mathbb{N}$$
74		simpr	$$⊢\left(\left(\left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)\wedge \forall b\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}\in \mathbb{N}\right)\wedge b\in \left({{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}\right)\right)\to b\in \left({{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}\right)$$
75	2	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)\wedge \forall e\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{j\in c}e\left(j\right)!}{\prod _{j\in c}e\left(j\right)!}\in \mathbb{N}\right)\wedge b\in \left({{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}\right)\right)\to A\in \mathrm{Fin}$$
76		simprl	$$⊢\left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)\to c\subseteq A$$
77	76	ad2antrr	$$⊢\left(\left(\left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)\wedge \forall e\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{j\in c}e\left(j\right)!}{\prod _{j\in c}e\left(j\right)!}\in \mathbb{N}\right)\wedge b\in \left({{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}\right)\right)\to c\subseteq A$$
78		simprr	$$⊢\left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)\to d\in \left(A\setminus c\right)$$
79	78	ad2antrr	$$⊢\left(\left(\left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)\wedge \forall e\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{j\in c}e\left(j\right)!}{\prod _{j\in c}e\left(j\right)!}\in \mathbb{N}\right)\wedge b\in \left({{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}\right)\right)\to d\in \left(A\setminus c\right)$$
80		simpr	$$⊢\left(\left(\left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)\wedge \forall e\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{j\in c}e\left(j\right)!}{\prod _{j\in c}e\left(j\right)!}\in \mathbb{N}\right)\wedge b\in \left({{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}\right)\right)\to b\in \left({{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}\right)$$
81		fveq2	$$⊢j=k\to e\left(j\right)=e\left(k\right)$$
82	81	cbvsumv	$$⊢\sum _{j\in c}e\left(j\right)=\sum _{k\in c}e\left(k\right)$$
83	82	fveq2i	$$⊢\sum _{j\in c}e\left(j\right)!=\sum _{k\in c}e\left(k\right)!$$
84		2fveq3	$$⊢j=k\to e\left(j\right)!=e\left(k\right)!$$
85	84	cbvprodv	$$⊢\prod _{j\in c}e\left(j\right)!=\prod _{k\in c}e\left(k\right)!$$
86	83 85	oveq12i	$$⊢\frac{\sum _{j\in c}e\left(j\right)!}{\prod _{j\in c}e\left(j\right)!}=\frac{\sum _{k\in c}e\left(k\right)!}{\prod _{k\in c}e\left(k\right)!}$$
87	86	eleq1i	$$⊢\frac{\sum _{j\in c}e\left(j\right)!}{\prod _{j\in c}e\left(j\right)!}\in \mathbb{N}\leftrightarrow \frac{\sum _{k\in c}e\left(k\right)!}{\prod _{k\in c}e\left(k\right)!}\in \mathbb{N}$$
88	87	ralbii	$$⊢\forall e\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{j\in c}e\left(j\right)!}{\prod _{j\in c}e\left(j\right)!}\in \mathbb{N}\leftrightarrow \forall e\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{k\in c}e\left(k\right)!}{\prod _{k\in c}e\left(k\right)!}\in \mathbb{N}$$
89	88	biimpi	$$⊢\forall e\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{j\in c}e\left(j\right)!}{\prod _{j\in c}e\left(j\right)!}\in \mathbb{N}\to \forall e\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{k\in c}e\left(k\right)!}{\prod _{k\in c}e\left(k\right)!}\in \mathbb{N}$$
90	89	ad2antlr	$$⊢\left(\left(\left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)\wedge \forall e\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{j\in c}e\left(j\right)!}{\prod _{j\in c}e\left(j\right)!}\in \mathbb{N}\right)\wedge b\in \left({{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}\right)\right)\to \forall e\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{k\in c}e\left(k\right)!}{\prod _{k\in c}e\left(k\right)!}\in \mathbb{N}$$
91	75 77 79 80 90	mccllem	$$⊢\left(\left(\left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)\wedge \forall e\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{j\in c}e\left(j\right)!}{\prod _{j\in c}e\left(j\right)!}\in \mathbb{N}\right)\wedge b\in \left({{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}\right)\right)\to \frac{\sum _{k\in c\cup \left\{d\right\}}b\left(k\right)!}{\prod _{k\in c\cup \left\{d\right\}}b\left(k\right)!}\in \mathbb{N}$$
92	55 73 74 91	syl21anc	$$⊢\left(\left(\left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)\wedge \forall b\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}\in \mathbb{N}\right)\wedge b\in \left({{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}\right)\right)\to \frac{\sum _{k\in c\cup \left\{d\right\}}b\left(k\right)!}{\prod _{k\in c\cup \left\{d\right\}}b\left(k\right)!}\in \mathbb{N}$$
93	92	ex	$$⊢\left(\left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)\wedge \forall b\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}\in \mathbb{N}\right)\to \left(b\in \left({{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}\right)\to \frac{\sum _{k\in c\cup \left\{d\right\}}b\left(k\right)!}{\prod _{k\in c\cup \left\{d\right\}}b\left(k\right)!}\in \mathbb{N}\right)$$
94	54 93	ralrimi	$$⊢\left(\left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)\wedge \forall b\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}\in \mathbb{N}\right)\to \forall b\in \left({{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}\right)\frac{\sum _{k\in c\cup \left\{d\right\}}b\left(k\right)!}{\prod _{k\in c\cup \left\{d\right\}}b\left(k\right)!}\in \mathbb{N}$$
95	94	ex	$$⊢\left(\phi \wedge \left(c\subseteq A\wedge d\in \left(A\setminus c\right)\right)\right)\to \left(\forall b\in \left({{\mathbb{N}}_0}^c\right)\frac{\sum _{k\in c}b\left(k\right)!}{\prod _{k\in c}b\left(k\right)!}\in \mathbb{N}\to \forall b\in \left({{\mathbb{N}}_0}^{\left(c\cup \left\{d\right\}\right)}\right)\frac{\sum _{k\in c\cup \left\{d\right\}}b\left(k\right)!}{\prod _{k\in c\cup \left\{d\right\}}b\left(k\right)!}\in \mathbb{N}\right)$$
96	12 21 30 39 51 95 2	findcard2d	$$⊢\phi \to \forall b\in \left({{\mathbb{N}}_0}^A\right)\frac{\sum _{k\in A}b\left(k\right)!}{\prod _{k\in A}b\left(k\right)!}\in \mathbb{N}$$
97		nfcv	$$⊢\underset{\_}{Ⅎ}kb$$
98	97 1	nfeq	$$⊢Ⅎkb=B$$
99		fveq1	$$⊢b=B\to b\left(k\right)=B\left(k\right)$$
100	99	a1d	$$⊢b=B\to \left(k\in A\to b\left(k\right)=B\left(k\right)\right)$$
101	98 100	ralrimi	$$⊢b=B\to \forall k\in Ab\left(k\right)=B\left(k\right)$$
102	101	sumeq2d	$$⊢b=B\to \sum _{k\in A}b\left(k\right)=\sum _{k\in A}B\left(k\right)$$
103	102	fveq2d	$$⊢b=B\to \sum _{k\in A}b\left(k\right)!=\sum _{k\in A}B\left(k\right)!$$
104	99	fveq2d	$$⊢b=B\to b\left(k\right)!=B\left(k\right)!$$
105	104	a1d	$$⊢b=B\to \left(k\in A\to b\left(k\right)!=B\left(k\right)!\right)$$
106	98 105	ralrimi	$$⊢b=B\to \forall k\in Ab\left(k\right)!=B\left(k\right)!$$
107	106	prodeq2d	$$⊢b=B\to \prod _{k\in A}b\left(k\right)!=\prod _{k\in A}B\left(k\right)!$$
108	103 107	oveq12d	$$⊢b=B\to \frac{\sum _{k\in A}b\left(k\right)!}{\prod _{k\in A}b\left(k\right)!}=\frac{\sum _{k\in A}B\left(k\right)!}{\prod _{k\in A}B\left(k\right)!}$$
109	108	eleq1d	$$⊢b=B\to \left(\frac{\sum _{k\in A}b\left(k\right)!}{\prod _{k\in A}b\left(k\right)!}\in \mathbb{N}\leftrightarrow \frac{\sum _{k\in A}B\left(k\right)!}{\prod _{k\in A}B\left(k\right)!}\in \mathbb{N}\right)$$
110	109	rspccva	$$⊢\left(\forall b\in \left({{\mathbb{N}}_0}^A\right)\frac{\sum _{k\in A}b\left(k\right)!}{\prod _{k\in A}b\left(k\right)!}\in \mathbb{N}\wedge B\in \left({{\mathbb{N}}_0}^A\right)\right)\to \frac{\sum _{k\in A}B\left(k\right)!}{\prod _{k\in A}B\left(k\right)!}\in \mathbb{N}$$
111	96 3 110	syl2anc	$$⊢\phi \to \frac{\sum _{k\in A}B\left(k\right)!}{\prod _{k\in A}B\left(k\right)!}\in \mathbb{N}$$