# Metamath Proof Explorer

## Theorem bcprod

Description: A product identity for binomial coefficents. (Contributed by Scott Fenton, 23-Jun-2020)

Ref Expression
Assertion bcprod ${⊢}{N}\in ℕ\to \prod _{{k}=1}^{{N}-1}\left(\genfrac{}{}{0}{}{{N}-1}{{k}}\right)=\prod _{{k}=1}^{{N}-1}{{k}}^{2{k}-{N}}$

### Proof

Step Hyp Ref Expression
1 oveq1 ${⊢}{m}=1\to {m}-1=1-1$
2 1m1e0 ${⊢}1-1=0$
3 1 2 syl6eq ${⊢}{m}=1\to {m}-1=0$
4 3 oveq2d ${⊢}{m}=1\to \left(1\dots {m}-1\right)=\left(1\dots 0\right)$
5 fz10 ${⊢}\left(1\dots 0\right)=\varnothing$
6 4 5 syl6eq ${⊢}{m}=1\to \left(1\dots {m}-1\right)=\varnothing$
7 3 oveq1d ${⊢}{m}=1\to \left(\genfrac{}{}{0}{}{{m}-1}{{k}}\right)=\left(\genfrac{}{}{0}{}{0}{{k}}\right)$
8 7 adantr ${⊢}\left({m}=1\wedge {k}\in \left(1\dots {m}-1\right)\right)\to \left(\genfrac{}{}{0}{}{{m}-1}{{k}}\right)=\left(\genfrac{}{}{0}{}{0}{{k}}\right)$
9 6 8 prodeq12dv ${⊢}{m}=1\to \prod _{{k}=1}^{{m}-1}\left(\genfrac{}{}{0}{}{{m}-1}{{k}}\right)=\prod _{{k}\in \varnothing }\left(\genfrac{}{}{0}{}{0}{{k}}\right)$
10 oveq2 ${⊢}{m}=1\to 2{k}-{m}=2{k}-1$
11 10 oveq2d ${⊢}{m}=1\to {{k}}^{2{k}-{m}}={{k}}^{2{k}-1}$
12 11 adantr ${⊢}\left({m}=1\wedge {k}\in \left(1\dots {m}-1\right)\right)\to {{k}}^{2{k}-{m}}={{k}}^{2{k}-1}$
13 6 12 prodeq12dv ${⊢}{m}=1\to \prod _{{k}=1}^{{m}-1}{{k}}^{2{k}-{m}}=\prod _{{k}\in \varnothing }{{k}}^{2{k}-1}$
14 9 13 eqeq12d ${⊢}{m}=1\to \left(\prod _{{k}=1}^{{m}-1}\left(\genfrac{}{}{0}{}{{m}-1}{{k}}\right)=\prod _{{k}=1}^{{m}-1}{{k}}^{2{k}-{m}}↔\prod _{{k}\in \varnothing }\left(\genfrac{}{}{0}{}{0}{{k}}\right)=\prod _{{k}\in \varnothing }{{k}}^{2{k}-1}\right)$
15 oveq1 ${⊢}{m}={n}\to {m}-1={n}-1$
16 15 oveq2d ${⊢}{m}={n}\to \left(1\dots {m}-1\right)=\left(1\dots {n}-1\right)$
17 15 oveq1d ${⊢}{m}={n}\to \left(\genfrac{}{}{0}{}{{m}-1}{{k}}\right)=\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)$
18 17 adantr ${⊢}\left({m}={n}\wedge {k}\in \left(1\dots {m}-1\right)\right)\to \left(\genfrac{}{}{0}{}{{m}-1}{{k}}\right)=\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)$
19 16 18 prodeq12dv ${⊢}{m}={n}\to \prod _{{k}=1}^{{m}-1}\left(\genfrac{}{}{0}{}{{m}-1}{{k}}\right)=\prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)$
20 oveq2 ${⊢}{m}={n}\to 2{k}-{m}=2{k}-{n}$
21 20 oveq2d ${⊢}{m}={n}\to {{k}}^{2{k}-{m}}={{k}}^{2{k}-{n}}$
22 21 adantr ${⊢}\left({m}={n}\wedge {k}\in \left(1\dots {m}-1\right)\right)\to {{k}}^{2{k}-{m}}={{k}}^{2{k}-{n}}$
23 16 22 prodeq12dv ${⊢}{m}={n}\to \prod _{{k}=1}^{{m}-1}{{k}}^{2{k}-{m}}=\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}$
24 19 23 eqeq12d ${⊢}{m}={n}\to \left(\prod _{{k}=1}^{{m}-1}\left(\genfrac{}{}{0}{}{{m}-1}{{k}}\right)=\prod _{{k}=1}^{{m}-1}{{k}}^{2{k}-{m}}↔\prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)=\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}\right)$
25 oveq1 ${⊢}{m}={n}+1\to {m}-1={n}+1-1$
26 25 oveq2d ${⊢}{m}={n}+1\to \left(1\dots {m}-1\right)=\left(1\dots {n}+1-1\right)$
27 25 oveq1d ${⊢}{m}={n}+1\to \left(\genfrac{}{}{0}{}{{m}-1}{{k}}\right)=\left(\genfrac{}{}{0}{}{{n}+1-1}{{k}}\right)$
28 27 adantr ${⊢}\left({m}={n}+1\wedge {k}\in \left(1\dots {m}-1\right)\right)\to \left(\genfrac{}{}{0}{}{{m}-1}{{k}}\right)=\left(\genfrac{}{}{0}{}{{n}+1-1}{{k}}\right)$
29 26 28 prodeq12dv ${⊢}{m}={n}+1\to \prod _{{k}=1}^{{m}-1}\left(\genfrac{}{}{0}{}{{m}-1}{{k}}\right)=\prod _{{k}=1}^{{n}+1-1}\left(\genfrac{}{}{0}{}{{n}+1-1}{{k}}\right)$
30 oveq2 ${⊢}{m}={n}+1\to 2{k}-{m}=2{k}-\left({n}+1\right)$
31 30 oveq2d ${⊢}{m}={n}+1\to {{k}}^{2{k}-{m}}={{k}}^{2{k}-\left({n}+1\right)}$
32 31 adantr ${⊢}\left({m}={n}+1\wedge {k}\in \left(1\dots {m}-1\right)\right)\to {{k}}^{2{k}-{m}}={{k}}^{2{k}-\left({n}+1\right)}$
33 26 32 prodeq12dv ${⊢}{m}={n}+1\to \prod _{{k}=1}^{{m}-1}{{k}}^{2{k}-{m}}=\prod _{{k}=1}^{{n}+1-1}{{k}}^{2{k}-\left({n}+1\right)}$
34 29 33 eqeq12d ${⊢}{m}={n}+1\to \left(\prod _{{k}=1}^{{m}-1}\left(\genfrac{}{}{0}{}{{m}-1}{{k}}\right)=\prod _{{k}=1}^{{m}-1}{{k}}^{2{k}-{m}}↔\prod _{{k}=1}^{{n}+1-1}\left(\genfrac{}{}{0}{}{{n}+1-1}{{k}}\right)=\prod _{{k}=1}^{{n}+1-1}{{k}}^{2{k}-\left({n}+1\right)}\right)$
35 oveq1 ${⊢}{m}={N}\to {m}-1={N}-1$
36 35 oveq2d ${⊢}{m}={N}\to \left(1\dots {m}-1\right)=\left(1\dots {N}-1\right)$
37 35 oveq1d ${⊢}{m}={N}\to \left(\genfrac{}{}{0}{}{{m}-1}{{k}}\right)=\left(\genfrac{}{}{0}{}{{N}-1}{{k}}\right)$
38 37 adantr ${⊢}\left({m}={N}\wedge {k}\in \left(1\dots {m}-1\right)\right)\to \left(\genfrac{}{}{0}{}{{m}-1}{{k}}\right)=\left(\genfrac{}{}{0}{}{{N}-1}{{k}}\right)$
39 36 38 prodeq12dv ${⊢}{m}={N}\to \prod _{{k}=1}^{{m}-1}\left(\genfrac{}{}{0}{}{{m}-1}{{k}}\right)=\prod _{{k}=1}^{{N}-1}\left(\genfrac{}{}{0}{}{{N}-1}{{k}}\right)$
40 oveq2 ${⊢}{m}={N}\to 2{k}-{m}=2{k}-{N}$
41 40 oveq2d ${⊢}{m}={N}\to {{k}}^{2{k}-{m}}={{k}}^{2{k}-{N}}$
42 41 adantr ${⊢}\left({m}={N}\wedge {k}\in \left(1\dots {m}-1\right)\right)\to {{k}}^{2{k}-{m}}={{k}}^{2{k}-{N}}$
43 36 42 prodeq12dv ${⊢}{m}={N}\to \prod _{{k}=1}^{{m}-1}{{k}}^{2{k}-{m}}=\prod _{{k}=1}^{{N}-1}{{k}}^{2{k}-{N}}$
44 39 43 eqeq12d ${⊢}{m}={N}\to \left(\prod _{{k}=1}^{{m}-1}\left(\genfrac{}{}{0}{}{{m}-1}{{k}}\right)=\prod _{{k}=1}^{{m}-1}{{k}}^{2{k}-{m}}↔\prod _{{k}=1}^{{N}-1}\left(\genfrac{}{}{0}{}{{N}-1}{{k}}\right)=\prod _{{k}=1}^{{N}-1}{{k}}^{2{k}-{N}}\right)$
45 prod0 ${⊢}\prod _{{k}\in \varnothing }\left(\genfrac{}{}{0}{}{0}{{k}}\right)=1$
46 prod0 ${⊢}\prod _{{k}\in \varnothing }{{k}}^{2{k}-1}=1$
47 45 46 eqtr4i ${⊢}\prod _{{k}\in \varnothing }\left(\genfrac{}{}{0}{}{0}{{k}}\right)=\prod _{{k}\in \varnothing }{{k}}^{2{k}-1}$
48 simpr ${⊢}\left({n}\in ℕ\wedge \prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)=\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}\right)\to \prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)=\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}$
49 48 oveq1d ${⊢}\left({n}\in ℕ\wedge \prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)=\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}\right)\to \prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)\left(\frac{{{n}}^{{n}-1}}{\left({n}-1\right)!}\right)=\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}\left(\frac{{{n}}^{{n}-1}}{\left({n}-1\right)!}\right)$
50 nncn ${⊢}{n}\in ℕ\to {n}\in ℂ$
51 1cnd ${⊢}{n}\in ℕ\to 1\in ℂ$
52 50 51 pncand ${⊢}{n}\in ℕ\to {n}+1-1={n}$
53 52 oveq2d ${⊢}{n}\in ℕ\to \left(1\dots {n}+1-1\right)=\left(1\dots {n}\right)$
54 52 oveq1d ${⊢}{n}\in ℕ\to \left(\genfrac{}{}{0}{}{{n}+1-1}{{k}}\right)=\left(\genfrac{}{}{0}{}{{n}}{{k}}\right)$
55 54 adantr ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}+1-1\right)\right)\to \left(\genfrac{}{}{0}{}{{n}+1-1}{{k}}\right)=\left(\genfrac{}{}{0}{}{{n}}{{k}}\right)$
56 53 55 prodeq12dv ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}+1-1}\left(\genfrac{}{}{0}{}{{n}+1-1}{{k}}\right)=\prod _{{k}=1}^{{n}}\left(\genfrac{}{}{0}{}{{n}}{{k}}\right)$
57 elnnuz ${⊢}{n}\in ℕ↔{n}\in {ℤ}_{\ge 1}$
58 57 biimpi ${⊢}{n}\in ℕ\to {n}\in {ℤ}_{\ge 1}$
59 nnnn0 ${⊢}{n}\in ℕ\to {n}\in {ℕ}_{0}$
60 elfzelz ${⊢}{k}\in \left(1\dots {n}\right)\to {k}\in ℤ$
61 bccl ${⊢}\left({n}\in {ℕ}_{0}\wedge {k}\in ℤ\right)\to \left(\genfrac{}{}{0}{}{{n}}{{k}}\right)\in {ℕ}_{0}$
62 59 60 61 syl2an ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}\right)\right)\to \left(\genfrac{}{}{0}{}{{n}}{{k}}\right)\in {ℕ}_{0}$
63 62 nn0cnd ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}\right)\right)\to \left(\genfrac{}{}{0}{}{{n}}{{k}}\right)\in ℂ$
64 oveq2 ${⊢}{k}={n}\to \left(\genfrac{}{}{0}{}{{n}}{{k}}\right)=\left(\genfrac{}{}{0}{}{{n}}{{n}}\right)$
65 58 63 64 fprodm1 ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}}\left(\genfrac{}{}{0}{}{{n}}{{k}}\right)=\prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}}{{k}}\right)\left(\genfrac{}{}{0}{}{{n}}{{n}}\right)$
66 bcnn ${⊢}{n}\in {ℕ}_{0}\to \left(\genfrac{}{}{0}{}{{n}}{{n}}\right)=1$
67 59 66 syl ${⊢}{n}\in ℕ\to \left(\genfrac{}{}{0}{}{{n}}{{n}}\right)=1$
68 67 oveq2d ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}}{{k}}\right)\left(\genfrac{}{}{0}{}{{n}}{{n}}\right)=\prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}}{{k}}\right)\cdot 1$
69 fzfid ${⊢}{n}\in ℕ\to \left(1\dots {n}-1\right)\in \mathrm{Fin}$
70 elfzelz ${⊢}{k}\in \left(1\dots {n}-1\right)\to {k}\in ℤ$
71 59 70 61 syl2an ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to \left(\genfrac{}{}{0}{}{{n}}{{k}}\right)\in {ℕ}_{0}$
72 71 nn0cnd ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to \left(\genfrac{}{}{0}{}{{n}}{{k}}\right)\in ℂ$
73 69 72 fprodcl ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}}{{k}}\right)\in ℂ$
74 73 mulid1d ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}}{{k}}\right)\cdot 1=\prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}}{{k}}\right)$
75 fz1ssfz0 ${⊢}\left(1\dots {n}-1\right)\subseteq \left(0\dots {n}-1\right)$
76 75 sseli ${⊢}{k}\in \left(1\dots {n}-1\right)\to {k}\in \left(0\dots {n}-1\right)$
77 bcm1nt ${⊢}\left({n}\in ℕ\wedge {k}\in \left(0\dots {n}-1\right)\right)\to \left(\genfrac{}{}{0}{}{{n}}{{k}}\right)=\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)\left(\frac{{n}}{{n}-{k}}\right)$
78 76 77 sylan2 ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to \left(\genfrac{}{}{0}{}{{n}}{{k}}\right)=\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)\left(\frac{{n}}{{n}-{k}}\right)$
79 78 prodeq2dv ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}}{{k}}\right)=\prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)\left(\frac{{n}}{{n}-{k}}\right)$
80 nnm1nn0 ${⊢}{n}\in ℕ\to {n}-1\in {ℕ}_{0}$
81 bccl ${⊢}\left({n}-1\in {ℕ}_{0}\wedge {k}\in ℤ\right)\to \left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)\in {ℕ}_{0}$
82 80 70 81 syl2an ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to \left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)\in {ℕ}_{0}$
83 82 nn0cnd ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to \left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)\in ℂ$
84 50 adantr ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {n}\in ℂ$
85 elfznn ${⊢}{k}\in \left(1\dots {n}-1\right)\to {k}\in ℕ$
86 85 adantl ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {k}\in ℕ$
87 86 nnred ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {k}\in ℝ$
88 80 adantr ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {n}-1\in {ℕ}_{0}$
89 88 nn0red ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {n}-1\in ℝ$
90 nnre ${⊢}{n}\in ℕ\to {n}\in ℝ$
91 90 adantr ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {n}\in ℝ$
92 elfzle2 ${⊢}{k}\in \left(1\dots {n}-1\right)\to {k}\le {n}-1$
93 92 adantl ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {k}\le {n}-1$
94 91 ltm1d ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {n}-1<{n}$
95 87 89 91 93 94 lelttrd ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {k}<{n}$
96 simpl ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {n}\in ℕ$
97 nnsub ${⊢}\left({k}\in ℕ\wedge {n}\in ℕ\right)\to \left({k}<{n}↔{n}-{k}\in ℕ\right)$
98 86 96 97 syl2anc ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to \left({k}<{n}↔{n}-{k}\in ℕ\right)$
99 95 98 mpbid ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {n}-{k}\in ℕ$
100 99 nncnd ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {n}-{k}\in ℂ$
101 99 nnne0d ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {n}-{k}\ne 0$
102 84 100 101 divcld ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to \frac{{n}}{{n}-{k}}\in ℂ$
103 69 83 102 fprodmul ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)\left(\frac{{n}}{{n}-{k}}\right)=\prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)\prod _{{k}=1}^{{n}-1}\left(\frac{{n}}{{n}-{k}}\right)$
104 69 84 100 101 fproddiv ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}-1}\left(\frac{{n}}{{n}-{k}}\right)=\frac{\prod _{{k}=1}^{{n}-1}{n}}{\prod _{{k}=1}^{{n}-1}\left({n}-{k}\right)}$
105 fzfi ${⊢}\left(1\dots {n}-1\right)\in \mathrm{Fin}$
106 fprodconst ${⊢}\left(\left(1\dots {n}-1\right)\in \mathrm{Fin}\wedge {n}\in ℂ\right)\to \prod _{{k}=1}^{{n}-1}{n}={{n}}^{\left|\left(1\dots {n}-1\right)\right|}$
107 105 50 106 sylancr ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}-1}{n}={{n}}^{\left|\left(1\dots {n}-1\right)\right|}$
108 hashfz1 ${⊢}{n}-1\in {ℕ}_{0}\to \left|\left(1\dots {n}-1\right)\right|={n}-1$
109 80 108 syl ${⊢}{n}\in ℕ\to \left|\left(1\dots {n}-1\right)\right|={n}-1$
110 109 oveq2d ${⊢}{n}\in ℕ\to {{n}}^{\left|\left(1\dots {n}-1\right)\right|}={{n}}^{{n}-1}$
111 107 110 eqtr2d ${⊢}{n}\in ℕ\to {{n}}^{{n}-1}=\prod _{{k}=1}^{{n}-1}{n}$
112 fprodfac ${⊢}{n}-1\in {ℕ}_{0}\to \left({n}-1\right)!=\prod _{{j}=1}^{{n}-1}{j}$
113 80 112 syl ${⊢}{n}\in ℕ\to \left({n}-1\right)!=\prod _{{j}=1}^{{n}-1}{j}$
114 nnz ${⊢}{n}\in ℕ\to {n}\in ℤ$
115 1zzd ${⊢}{n}\in ℕ\to 1\in ℤ$
116 80 nn0zd ${⊢}{n}\in ℕ\to {n}-1\in ℤ$
117 elfznn ${⊢}{j}\in \left(1\dots {n}-1\right)\to {j}\in ℕ$
118 117 adantl ${⊢}\left({n}\in ℕ\wedge {j}\in \left(1\dots {n}-1\right)\right)\to {j}\in ℕ$
119 118 nncnd ${⊢}\left({n}\in ℕ\wedge {j}\in \left(1\dots {n}-1\right)\right)\to {j}\in ℂ$
120 id ${⊢}{j}={n}-{k}\to {j}={n}-{k}$
121 114 115 116 119 120 fprodrev ${⊢}{n}\in ℕ\to \prod _{{j}=1}^{{n}-1}{j}=\prod _{{k}={n}-\left({n}-1\right)}^{{n}-1}\left({n}-{k}\right)$
122 50 51 nncand ${⊢}{n}\in ℕ\to {n}-\left({n}-1\right)=1$
123 122 oveq1d ${⊢}{n}\in ℕ\to \left({n}-\left({n}-1\right)\dots {n}-1\right)=\left(1\dots {n}-1\right)$
124 123 prodeq1d ${⊢}{n}\in ℕ\to \prod _{{k}={n}-\left({n}-1\right)}^{{n}-1}\left({n}-{k}\right)=\prod _{{k}=1}^{{n}-1}\left({n}-{k}\right)$
125 113 121 124 3eqtrd ${⊢}{n}\in ℕ\to \left({n}-1\right)!=\prod _{{k}=1}^{{n}-1}\left({n}-{k}\right)$
126 111 125 oveq12d ${⊢}{n}\in ℕ\to \frac{{{n}}^{{n}-1}}{\left({n}-1\right)!}=\frac{\prod _{{k}=1}^{{n}-1}{n}}{\prod _{{k}=1}^{{n}-1}\left({n}-{k}\right)}$
127 104 126 eqtr4d ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}-1}\left(\frac{{n}}{{n}-{k}}\right)=\frac{{{n}}^{{n}-1}}{\left({n}-1\right)!}$
128 127 oveq2d ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)\prod _{{k}=1}^{{n}-1}\left(\frac{{n}}{{n}-{k}}\right)=\prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)\left(\frac{{{n}}^{{n}-1}}{\left({n}-1\right)!}\right)$
129 79 103 128 3eqtrd ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}}{{k}}\right)=\prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)\left(\frac{{{n}}^{{n}-1}}{\left({n}-1\right)!}\right)$
130 68 74 129 3eqtrd ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}}{{k}}\right)\left(\genfrac{}{}{0}{}{{n}}{{n}}\right)=\prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)\left(\frac{{{n}}^{{n}-1}}{\left({n}-1\right)!}\right)$
131 56 65 130 3eqtrd ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}+1-1}\left(\genfrac{}{}{0}{}{{n}+1-1}{{k}}\right)=\prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)\left(\frac{{{n}}^{{n}-1}}{\left({n}-1\right)!}\right)$
132 131 adantr ${⊢}\left({n}\in ℕ\wedge \prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)=\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}\right)\to \prod _{{k}=1}^{{n}+1-1}\left(\genfrac{}{}{0}{}{{n}+1-1}{{k}}\right)=\prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)\left(\frac{{{n}}^{{n}-1}}{\left({n}-1\right)!}\right)$
133 53 prodeq1d ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}+1-1}{{k}}^{2{k}-\left({n}+1\right)}=\prod _{{k}=1}^{{n}}{{k}}^{2{k}-\left({n}+1\right)}$
134 elfznn ${⊢}{k}\in \left(1\dots {n}\right)\to {k}\in ℕ$
135 134 adantl ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}\right)\right)\to {k}\in ℕ$
136 135 nncnd ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}\right)\right)\to {k}\in ℂ$
137 135 nnne0d ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}\right)\right)\to {k}\ne 0$
138 2nn ${⊢}2\in ℕ$
139 138 a1i ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}\right)\right)\to 2\in ℕ$
140 139 135 nnmulcld ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}\right)\right)\to 2{k}\in ℕ$
141 140 nnzd ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}\right)\right)\to 2{k}\in ℤ$
142 peano2nn ${⊢}{n}\in ℕ\to {n}+1\in ℕ$
143 142 adantr ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}\right)\right)\to {n}+1\in ℕ$
144 143 nnzd ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}\right)\right)\to {n}+1\in ℤ$
145 141 144 zsubcld ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}\right)\right)\to 2{k}-\left({n}+1\right)\in ℤ$
146 136 137 145 expclzd ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}\right)\right)\to {{k}}^{2{k}-\left({n}+1\right)}\in ℂ$
147 id ${⊢}{k}={n}\to {k}={n}$
148 oveq2 ${⊢}{k}={n}\to 2{k}=2{n}$
149 148 oveq1d ${⊢}{k}={n}\to 2{k}-\left({n}+1\right)=2{n}-\left({n}+1\right)$
150 147 149 oveq12d ${⊢}{k}={n}\to {{k}}^{2{k}-\left({n}+1\right)}={{n}}^{2{n}-\left({n}+1\right)}$
151 58 146 150 fprodm1 ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}}{{k}}^{2{k}-\left({n}+1\right)}=\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-\left({n}+1\right)}{{n}}^{2{n}-\left({n}+1\right)}$
152 86 nncnd ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {k}\in ℂ$
153 86 nnne0d ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {k}\ne 0$
154 138 a1i ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to 2\in ℕ$
155 154 86 nnmulcld ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to 2{k}\in ℕ$
156 155 nnzd ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to 2{k}\in ℤ$
157 114 adantr ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {n}\in ℤ$
158 156 157 zsubcld ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to 2{k}-{n}\in ℤ$
159 152 153 158 expclzd ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {{k}}^{2{k}-{n}}\in ℂ$
160 69 159 152 153 fproddiv ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}-1}\left(\frac{{{k}}^{2{k}-{n}}}{{k}}\right)=\frac{\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}}{\prod _{{k}=1}^{{n}-1}{k}}$
161 155 nncnd ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to 2{k}\in ℂ$
162 1cnd ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to 1\in ℂ$
163 161 84 162 subsub4d ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to 2{k}-{n}-1=2{k}-\left({n}+1\right)$
164 163 oveq2d ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {{k}}^{2{k}-{n}-1}={{k}}^{2{k}-\left({n}+1\right)}$
165 152 153 158 expm1d ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {{k}}^{2{k}-{n}-1}=\frac{{{k}}^{2{k}-{n}}}{{k}}$
166 164 165 eqtr3d ${⊢}\left({n}\in ℕ\wedge {k}\in \left(1\dots {n}-1\right)\right)\to {{k}}^{2{k}-\left({n}+1\right)}=\frac{{{k}}^{2{k}-{n}}}{{k}}$
167 166 prodeq2dv ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-\left({n}+1\right)}=\prod _{{k}=1}^{{n}-1}\left(\frac{{{k}}^{2{k}-{n}}}{{k}}\right)$
168 fprodfac ${⊢}{n}-1\in {ℕ}_{0}\to \left({n}-1\right)!=\prod _{{k}=1}^{{n}-1}{k}$
169 80 168 syl ${⊢}{n}\in ℕ\to \left({n}-1\right)!=\prod _{{k}=1}^{{n}-1}{k}$
170 169 oveq2d ${⊢}{n}\in ℕ\to \frac{\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}}{\left({n}-1\right)!}=\frac{\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}}{\prod _{{k}=1}^{{n}-1}{k}}$
171 160 167 170 3eqtr4d ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-\left({n}+1\right)}=\frac{\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}}{\left({n}-1\right)!}$
172 138 a1i ${⊢}{n}\in ℕ\to 2\in ℕ$
173 id ${⊢}{n}\in ℕ\to {n}\in ℕ$
174 172 173 nnmulcld ${⊢}{n}\in ℕ\to 2{n}\in ℕ$
175 174 nncnd ${⊢}{n}\in ℕ\to 2{n}\in ℂ$
176 175 50 51 subsub4d ${⊢}{n}\in ℕ\to 2{n}-{n}-1=2{n}-\left({n}+1\right)$
177 50 2timesd ${⊢}{n}\in ℕ\to 2{n}={n}+{n}$
178 50 50 177 mvrladdd ${⊢}{n}\in ℕ\to 2{n}-{n}={n}$
179 178 oveq1d ${⊢}{n}\in ℕ\to 2{n}-{n}-1={n}-1$
180 176 179 eqtr3d ${⊢}{n}\in ℕ\to 2{n}-\left({n}+1\right)={n}-1$
181 180 oveq2d ${⊢}{n}\in ℕ\to {{n}}^{2{n}-\left({n}+1\right)}={{n}}^{{n}-1}$
182 171 181 oveq12d ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-\left({n}+1\right)}{{n}}^{2{n}-\left({n}+1\right)}=\left(\frac{\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}}{\left({n}-1\right)!}\right){{n}}^{{n}-1}$
183 69 159 fprodcl ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}\in ℂ$
184 faccl ${⊢}{n}-1\in {ℕ}_{0}\to \left({n}-1\right)!\in ℕ$
185 80 184 syl ${⊢}{n}\in ℕ\to \left({n}-1\right)!\in ℕ$
186 185 nncnd ${⊢}{n}\in ℕ\to \left({n}-1\right)!\in ℂ$
187 50 80 expcld ${⊢}{n}\in ℕ\to {{n}}^{{n}-1}\in ℂ$
188 185 nnne0d ${⊢}{n}\in ℕ\to \left({n}-1\right)!\ne 0$
189 183 186 187 188 div32d ${⊢}{n}\in ℕ\to \left(\frac{\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}}{\left({n}-1\right)!}\right){{n}}^{{n}-1}=\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}\left(\frac{{{n}}^{{n}-1}}{\left({n}-1\right)!}\right)$
190 182 189 eqtrd ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-\left({n}+1\right)}{{n}}^{2{n}-\left({n}+1\right)}=\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}\left(\frac{{{n}}^{{n}-1}}{\left({n}-1\right)!}\right)$
191 133 151 190 3eqtrd ${⊢}{n}\in ℕ\to \prod _{{k}=1}^{{n}+1-1}{{k}}^{2{k}-\left({n}+1\right)}=\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}\left(\frac{{{n}}^{{n}-1}}{\left({n}-1\right)!}\right)$
192 191 adantr ${⊢}\left({n}\in ℕ\wedge \prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)=\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}\right)\to \prod _{{k}=1}^{{n}+1-1}{{k}}^{2{k}-\left({n}+1\right)}=\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}\left(\frac{{{n}}^{{n}-1}}{\left({n}-1\right)!}\right)$
193 49 132 192 3eqtr4d ${⊢}\left({n}\in ℕ\wedge \prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)=\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}\right)\to \prod _{{k}=1}^{{n}+1-1}\left(\genfrac{}{}{0}{}{{n}+1-1}{{k}}\right)=\prod _{{k}=1}^{{n}+1-1}{{k}}^{2{k}-\left({n}+1\right)}$
194 193 ex ${⊢}{n}\in ℕ\to \left(\prod _{{k}=1}^{{n}-1}\left(\genfrac{}{}{0}{}{{n}-1}{{k}}\right)=\prod _{{k}=1}^{{n}-1}{{k}}^{2{k}-{n}}\to \prod _{{k}=1}^{{n}+1-1}\left(\genfrac{}{}{0}{}{{n}+1-1}{{k}}\right)=\prod _{{k}=1}^{{n}+1-1}{{k}}^{2{k}-\left({n}+1\right)}\right)$
195 14 24 34 44 47 194 nnind ${⊢}{N}\in ℕ\to \prod _{{k}=1}^{{N}-1}\left(\genfrac{}{}{0}{}{{N}-1}{{k}}\right)=\prod _{{k}=1}^{{N}-1}{{k}}^{2{k}-{N}}$