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

Metamath Proof Explorer

Theorem bcprod

Proof