# Metamath Proof Explorer

## 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{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{B}$
mccl.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
mccl.b ${⊢}{\phi }\to {B}\in \left({{ℕ}_{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 ℕ$

### Proof

Step Hyp Ref Expression
1 mccl.kb ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{B}$
2 mccl.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
3 mccl.b ${⊢}{\phi }\to {B}\in \left({{ℕ}_{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 ℕ↔\frac{\sum _{{k}\in \varnothing }{b}\left({k}\right)!}{\prod _{{k}\in \varnothing }{b}\left({k}\right)!}\in ℕ\right)$
9 8 ralbidv ${⊢}{a}=\varnothing \to \left(\forall {b}\in \left({{ℕ}_{0}}^{{a}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {a}}{b}\left({k}\right)!}{\prod _{{k}\in {a}}{b}\left({k}\right)!}\in ℕ↔\forall {b}\in \left({{ℕ}_{0}}^{{a}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in \varnothing }{b}\left({k}\right)!}{\prod _{{k}\in \varnothing }{b}\left({k}\right)!}\in ℕ\right)$
10 oveq2 ${⊢}{a}=\varnothing \to {{ℕ}_{0}}^{{a}}={{ℕ}_{0}}^{\varnothing }$
11 10 raleqdv ${⊢}{a}=\varnothing \to \left(\forall {b}\in \left({{ℕ}_{0}}^{{a}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in \varnothing }{b}\left({k}\right)!}{\prod _{{k}\in \varnothing }{b}\left({k}\right)!}\in ℕ↔\forall {b}\in \left({{ℕ}_{0}}^{\varnothing }\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in \varnothing }{b}\left({k}\right)!}{\prod _{{k}\in \varnothing }{b}\left({k}\right)!}\in ℕ\right)$
12 9 11 bitrd ${⊢}{a}=\varnothing \to \left(\forall {b}\in \left({{ℕ}_{0}}^{{a}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {a}}{b}\left({k}\right)!}{\prod _{{k}\in {a}}{b}\left({k}\right)!}\in ℕ↔\forall {b}\in \left({{ℕ}_{0}}^{\varnothing }\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in \varnothing }{b}\left({k}\right)!}{\prod _{{k}\in \varnothing }{b}\left({k}\right)!}\in ℕ\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 ℕ↔\frac{\sum _{{k}\in {c}}{b}\left({k}\right)!}{\prod _{{k}\in {c}}{b}\left({k}\right)!}\in ℕ\right)$
18 17 ralbidv ${⊢}{a}={c}\to \left(\forall {b}\in \left({{ℕ}_{0}}^{{a}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {a}}{b}\left({k}\right)!}{\prod _{{k}\in {a}}{b}\left({k}\right)!}\in ℕ↔\forall {b}\in \left({{ℕ}_{0}}^{{a}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{b}\left({k}\right)!}{\prod _{{k}\in {c}}{b}\left({k}\right)!}\in ℕ\right)$
19 oveq2 ${⊢}{a}={c}\to {{ℕ}_{0}}^{{a}}={{ℕ}_{0}}^{{c}}$
20 19 raleqdv ${⊢}{a}={c}\to \left(\forall {b}\in \left({{ℕ}_{0}}^{{a}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{b}\left({k}\right)!}{\prod _{{k}\in {c}}{b}\left({k}\right)!}\in ℕ↔\forall {b}\in \left({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{b}\left({k}\right)!}{\prod _{{k}\in {c}}{b}\left({k}\right)!}\in ℕ\right)$
21 18 20 bitrd ${⊢}{a}={c}\to \left(\forall {b}\in \left({{ℕ}_{0}}^{{a}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {a}}{b}\left({k}\right)!}{\prod _{{k}\in {a}}{b}\left({k}\right)!}\in ℕ↔\forall {b}\in \left({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{b}\left({k}\right)!}{\prod _{{k}\in {c}}{b}\left({k}\right)!}\in ℕ\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 ℕ↔\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 ℕ\right)$
27 26 ralbidv ${⊢}{a}={c}\cup \left\{{d}\right\}\to \left(\forall {b}\in \left({{ℕ}_{0}}^{{a}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {a}}{b}\left({k}\right)!}{\prod _{{k}\in {a}}{b}\left({k}\right)!}\in ℕ↔\forall {b}\in \left({{ℕ}_{0}}^{{a}}\right)\phantom{\rule{.4em}{0ex}}\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 ℕ\right)$
28 oveq2 ${⊢}{a}={c}\cup \left\{{d}\right\}\to {{ℕ}_{0}}^{{a}}={{ℕ}_{0}}^{\left({c}\cup \left\{{d}\right\}\right)}$
29 28 raleqdv ${⊢}{a}={c}\cup \left\{{d}\right\}\to \left(\forall {b}\in \left({{ℕ}_{0}}^{{a}}\right)\phantom{\rule{.4em}{0ex}}\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 ℕ↔\forall {b}\in \left({{ℕ}_{0}}^{\left({c}\cup \left\{{d}\right\}\right)}\right)\phantom{\rule{.4em}{0ex}}\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 ℕ\right)$
30 27 29 bitrd ${⊢}{a}={c}\cup \left\{{d}\right\}\to \left(\forall {b}\in \left({{ℕ}_{0}}^{{a}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {a}}{b}\left({k}\right)!}{\prod _{{k}\in {a}}{b}\left({k}\right)!}\in ℕ↔\forall {b}\in \left({{ℕ}_{0}}^{\left({c}\cup \left\{{d}\right\}\right)}\right)\phantom{\rule{.4em}{0ex}}\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 ℕ\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 ℕ↔\frac{\sum _{{k}\in {A}}{b}\left({k}\right)!}{\prod _{{k}\in {A}}{b}\left({k}\right)!}\in ℕ\right)$
36 35 ralbidv ${⊢}{a}={A}\to \left(\forall {b}\in \left({{ℕ}_{0}}^{{a}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {a}}{b}\left({k}\right)!}{\prod _{{k}\in {a}}{b}\left({k}\right)!}\in ℕ↔\forall {b}\in \left({{ℕ}_{0}}^{{a}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {A}}{b}\left({k}\right)!}{\prod _{{k}\in {A}}{b}\left({k}\right)!}\in ℕ\right)$
37 oveq2 ${⊢}{a}={A}\to {{ℕ}_{0}}^{{a}}={{ℕ}_{0}}^{{A}}$
38 37 raleqdv ${⊢}{a}={A}\to \left(\forall {b}\in \left({{ℕ}_{0}}^{{a}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {A}}{b}\left({k}\right)!}{\prod _{{k}\in {A}}{b}\left({k}\right)!}\in ℕ↔\forall {b}\in \left({{ℕ}_{0}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {A}}{b}\left({k}\right)!}{\prod _{{k}\in {A}}{b}\left({k}\right)!}\in ℕ\right)$
39 36 38 bitrd ${⊢}{a}={A}\to \left(\forall {b}\in \left({{ℕ}_{0}}^{{a}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {a}}{b}\left({k}\right)!}{\prod _{{k}\in {a}}{b}\left({k}\right)!}\in ℕ↔\forall {b}\in \left({{ℕ}_{0}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {A}}{b}\left({k}\right)!}{\prod _{{k}\in {A}}{b}\left({k}\right)!}\in ℕ\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 ℕ$
49 47 48 eqeltri ${⊢}\frac{\sum _{{k}\in \varnothing }{b}\left({k}\right)!}{\prod _{{k}\in \varnothing }{b}\left({k}\right)!}\in ℕ$
50 49 a1i ${⊢}\left({\phi }\wedge {b}\in \left({{ℕ}_{0}}^{\varnothing }\right)\right)\to \frac{\sum _{{k}\in \varnothing }{b}\left({k}\right)!}{\prod _{{k}\in \varnothing }{b}\left({k}\right)!}\in ℕ$
51 50 ralrimiva ${⊢}{\phi }\to \forall {b}\in \left({{ℕ}_{0}}^{\varnothing }\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in \varnothing }{b}\left({k}\right)!}{\prod _{{k}\in \varnothing }{b}\left({k}\right)!}\in ℕ$
52 nfv ${⊢}Ⅎ{b}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \left({c}\subseteq {A}\wedge {d}\in \left({A}\setminus {c}\right)\right)\right)$
53 nfra1 ${⊢}Ⅎ{b}\phantom{\rule{.4em}{0ex}}\forall {b}\in \left({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{b}\left({k}\right)!}{\prod _{{k}\in {c}}{b}\left({k}\right)!}\in ℕ$
54 52 53 nfan ${⊢}Ⅎ{b}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge \left({c}\subseteq {A}\wedge {d}\in \left({A}\setminus {c}\right)\right)\right)\wedge \forall {b}\in \left({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{b}\left({k}\right)!}{\prod _{{k}\in {c}}{b}\left({k}\right)!}\in ℕ\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({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{b}\left({k}\right)!}{\prod _{{k}\in {c}}{b}\left({k}\right)!}\in ℕ\right)\wedge {b}\in \left({{ℕ}_{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 ℕ↔\frac{\sum _{{j}\in {c}}{e}\left({j}\right)!}{\prod _{{j}\in {c}}{e}\left({j}\right)!}\in ℕ\right)$
71 70 cbvralvw ${⊢}\forall {b}\in \left({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{b}\left({k}\right)!}{\prod _{{k}\in {c}}{b}\left({k}\right)!}\in ℕ↔\forall {e}\in \left({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{j}\in {c}}{e}\left({j}\right)!}{\prod _{{j}\in {c}}{e}\left({j}\right)!}\in ℕ$
72 71 biimpi ${⊢}\forall {b}\in \left({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{b}\left({k}\right)!}{\prod _{{k}\in {c}}{b}\left({k}\right)!}\in ℕ\to \forall {e}\in \left({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{j}\in {c}}{e}\left({j}\right)!}{\prod _{{j}\in {c}}{e}\left({j}\right)!}\in ℕ$
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({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{b}\left({k}\right)!}{\prod _{{k}\in {c}}{b}\left({k}\right)!}\in ℕ\right)\wedge {b}\in \left({{ℕ}_{0}}^{\left({c}\cup \left\{{d}\right\}\right)}\right)\right)\to \forall {e}\in \left({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{j}\in {c}}{e}\left({j}\right)!}{\prod _{{j}\in {c}}{e}\left({j}\right)!}\in ℕ$
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({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{b}\left({k}\right)!}{\prod _{{k}\in {c}}{b}\left({k}\right)!}\in ℕ\right)\wedge {b}\in \left({{ℕ}_{0}}^{\left({c}\cup \left\{{d}\right\}\right)}\right)\right)\to {b}\in \left({{ℕ}_{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({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{j}\in {c}}{e}\left({j}\right)!}{\prod _{{j}\in {c}}{e}\left({j}\right)!}\in ℕ\right)\wedge {b}\in \left({{ℕ}_{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({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{j}\in {c}}{e}\left({j}\right)!}{\prod _{{j}\in {c}}{e}\left({j}\right)!}\in ℕ\right)\wedge {b}\in \left({{ℕ}_{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({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{j}\in {c}}{e}\left({j}\right)!}{\prod _{{j}\in {c}}{e}\left({j}\right)!}\in ℕ\right)\wedge {b}\in \left({{ℕ}_{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({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{j}\in {c}}{e}\left({j}\right)!}{\prod _{{j}\in {c}}{e}\left({j}\right)!}\in ℕ\right)\wedge {b}\in \left({{ℕ}_{0}}^{\left({c}\cup \left\{{d}\right\}\right)}\right)\right)\to {b}\in \left({{ℕ}_{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 ℕ↔\frac{\sum _{{k}\in {c}}{e}\left({k}\right)!}{\prod _{{k}\in {c}}{e}\left({k}\right)!}\in ℕ$
88 87 ralbii ${⊢}\forall {e}\in \left({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{j}\in {c}}{e}\left({j}\right)!}{\prod _{{j}\in {c}}{e}\left({j}\right)!}\in ℕ↔\forall {e}\in \left({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{e}\left({k}\right)!}{\prod _{{k}\in {c}}{e}\left({k}\right)!}\in ℕ$
89 88 biimpi ${⊢}\forall {e}\in \left({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{j}\in {c}}{e}\left({j}\right)!}{\prod _{{j}\in {c}}{e}\left({j}\right)!}\in ℕ\to \forall {e}\in \left({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{e}\left({k}\right)!}{\prod _{{k}\in {c}}{e}\left({k}\right)!}\in ℕ$
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({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{j}\in {c}}{e}\left({j}\right)!}{\prod _{{j}\in {c}}{e}\left({j}\right)!}\in ℕ\right)\wedge {b}\in \left({{ℕ}_{0}}^{\left({c}\cup \left\{{d}\right\}\right)}\right)\right)\to \forall {e}\in \left({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{e}\left({k}\right)!}{\prod _{{k}\in {c}}{e}\left({k}\right)!}\in ℕ$
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({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{j}\in {c}}{e}\left({j}\right)!}{\prod _{{j}\in {c}}{e}\left({j}\right)!}\in ℕ\right)\wedge {b}\in \left({{ℕ}_{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 ℕ$
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({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{b}\left({k}\right)!}{\prod _{{k}\in {c}}{b}\left({k}\right)!}\in ℕ\right)\wedge {b}\in \left({{ℕ}_{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 ℕ$
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({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{b}\left({k}\right)!}{\prod _{{k}\in {c}}{b}\left({k}\right)!}\in ℕ\right)\to \left({b}\in \left({{ℕ}_{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 ℕ\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({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{b}\left({k}\right)!}{\prod _{{k}\in {c}}{b}\left({k}\right)!}\in ℕ\right)\to \forall {b}\in \left({{ℕ}_{0}}^{\left({c}\cup \left\{{d}\right\}\right)}\right)\phantom{\rule{.4em}{0ex}}\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 ℕ$
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({{ℕ}_{0}}^{{c}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {c}}{b}\left({k}\right)!}{\prod _{{k}\in {c}}{b}\left({k}\right)!}\in ℕ\to \forall {b}\in \left({{ℕ}_{0}}^{\left({c}\cup \left\{{d}\right\}\right)}\right)\phantom{\rule{.4em}{0ex}}\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 ℕ\right)$
96 12 21 30 39 51 95 2 findcard2d ${⊢}{\phi }\to \forall {b}\in \left({{ℕ}_{0}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {A}}{b}\left({k}\right)!}{\prod _{{k}\in {A}}{b}\left({k}\right)!}\in ℕ$
97 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{b}$
98 97 1 nfeq ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{b}={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 {A}\phantom{\rule{.4em}{0ex}}{b}\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 {A}\phantom{\rule{.4em}{0ex}}{b}\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 ℕ↔\frac{\sum _{{k}\in {A}}{B}\left({k}\right)!}{\prod _{{k}\in {A}}{B}\left({k}\right)!}\in ℕ\right)$
110 109 rspccva ${⊢}\left(\forall {b}\in \left({{ℕ}_{0}}^{{A}}\right)\phantom{\rule{.4em}{0ex}}\frac{\sum _{{k}\in {A}}{b}\left({k}\right)!}{\prod _{{k}\in {A}}{b}\left({k}\right)!}\in ℕ\wedge {B}\in \left({{ℕ}_{0}}^{{A}}\right)\right)\to \frac{\sum _{{k}\in {A}}{B}\left({k}\right)!}{\prod _{{k}\in {A}}{B}\left({k}\right)!}\in ℕ$
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 ℕ$