Metamath Proof Explorer

Theorem bcprod

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

Ref Expression
Assertion bcprod ⊢N∈ℕ→∏k=1N−1(N−1k)=∏k=1N−1k2⁢k−N

Proof

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