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 = 1 N 1 ( N 1 k) = k = 1 N 1 k 2 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 1 k) = ( 0 k)
8 7 adantr m = 1 k 1 m 1 ( m 1 k) = ( 0 k)
9 6 8 prodeq12dv m = 1 k = 1 m 1 ( m 1 k) = k ( 0 k)
10 oveq2 m = 1 2 k m = 2 k 1
11 10 oveq2d m = 1 k 2 k m = k 2 k 1
12 11 adantr m = 1 k 1 m 1 k 2 k m = k 2 k 1
13 6 12 prodeq12dv m = 1 k = 1 m 1 k 2 k m = k k 2 k 1
14 9 13 eqeq12d m = 1 k = 1 m 1 ( m 1 k) = k = 1 m 1 k 2 k m k ( 0 k) = k k 2 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 1 k) = ( n 1 k)
18 17 adantr m = n k 1 m 1 ( m 1 k) = ( n 1 k)
19 16 18 prodeq12dv m = n k = 1 m 1 ( m 1 k) = k = 1 n 1 ( n 1 k)
20 oveq2 m = n 2 k m = 2 k n
21 20 oveq2d m = n k 2 k m = k 2 k n
22 21 adantr m = n k 1 m 1 k 2 k m = k 2 k n
23 16 22 prodeq12dv m = n k = 1 m 1 k 2 k m = k = 1 n 1 k 2 k n
24 19 23 eqeq12d m = n k = 1 m 1 ( m 1 k) = k = 1 m 1 k 2 k m k = 1 n 1 ( n 1 k) = k = 1 n 1 k 2 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 1 k) = ( n + 1 - 1 k)
28 27 adantr m = n + 1 k 1 m 1 ( m 1 k) = ( n + 1 - 1 k)
29 26 28 prodeq12dv m = n + 1 k = 1 m 1 ( m 1 k) = k = 1 n + 1 - 1 ( n + 1 - 1 k)
30 oveq2 m = n + 1 2 k m = 2 k n + 1
31 30 oveq2d m = n + 1 k 2 k m = k 2 k n + 1
32 31 adantr m = n + 1 k 1 m 1 k 2 k m = k 2 k n + 1
33 26 32 prodeq12dv m = n + 1 k = 1 m 1 k 2 k m = k = 1 n + 1 - 1 k 2 k n + 1
34 29 33 eqeq12d m = n + 1 k = 1 m 1 ( m 1 k) = k = 1 m 1 k 2 k m k = 1 n + 1 - 1 ( n + 1 - 1 k) = k = 1 n + 1 - 1 k 2 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 1 k) = ( N 1 k)
38 37 adantr m = N k 1 m 1 ( m 1 k) = ( N 1 k)
39 36 38 prodeq12dv m = N k = 1 m 1 ( m 1 k) = k = 1 N 1 ( N 1 k)
40 oveq2 m = N 2 k m = 2 k N
41 40 oveq2d m = N k 2 k m = k 2 k N
42 41 adantr m = N k 1 m 1 k 2 k m = k 2 k N
43 36 42 prodeq12dv m = N k = 1 m 1 k 2 k m = k = 1 N 1 k 2 k N
44 39 43 eqeq12d m = N k = 1 m 1 ( m 1 k) = k = 1 m 1 k 2 k m k = 1 N 1 ( N 1 k) = k = 1 N 1 k 2 k N
45 prod0 k ( 0 k) = 1
46 prod0 k k 2 k 1 = 1
47 45 46 eqtr4i k ( 0 k) = k k 2 k 1
48 simpr n k = 1 n 1 ( n 1 k) = k = 1 n 1 k 2 k n k = 1 n 1 ( n 1 k) = k = 1 n 1 k 2 k n
49 48 oveq1d n k = 1 n 1 ( n 1 k) = k = 1 n 1 k 2 k n k = 1 n 1 ( n 1 k) n n 1 n 1 ! = k = 1 n 1 k 2 k n n n 1 n 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 - 1 k) = ( n k)
55 54 adantr n k 1 n + 1 - 1 ( n + 1 - 1 k) = ( n k)
56 53 55 prodeq12dv n k = 1 n + 1 - 1 ( n + 1 - 1 k) = k = 1 n ( n k)
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 ( n k) 0
62 59 60 61 syl2an n k 1 n ( n k) 0
63 62 nn0cnd n k 1 n ( n k)
64 oveq2 k = n ( n k) = ( n n)
65 58 63 64 fprodm1 n k = 1 n ( n k) = k = 1 n 1 ( n k) ( n n)
66 bcnn n 0 ( n n) = 1
67 59 66 syl n ( n n) = 1
68 67 oveq2d n k = 1 n 1 ( n k) ( n n) = k = 1 n 1 ( n k) 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 ( n k) 0
72 71 nn0cnd n k 1 n 1 ( n k)
73 69 72 fprodcl n k = 1 n 1 ( n k)
74 73 mulid1d n k = 1 n 1 ( n k) 1 = k = 1 n 1 ( n k)
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 ( n k) = ( n 1 k) n n k
78 76 77 sylan2 n k 1 n 1 ( n k) = ( n 1 k) n n k
79 78 prodeq2dv n k = 1 n 1 ( n k) = k = 1 n 1 ( n 1 k) n n k
80 nnm1nn0 n n 1 0
81 bccl n 1 0 k ( n 1 k) 0
82 80 70 81 syl2an n k 1 n 1 ( n 1 k) 0
83 82 nn0cnd n k 1 n 1 ( n 1 k)
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 n n k
103 69 83 102 fprodmul n k = 1 n 1 ( n 1 k) n n k = k = 1 n 1 ( n 1 k) k = 1 n 1 n n k
104 69 84 100 101 fproddiv n k = 1 n 1 n n k = k = 1 n 1 n k = 1 n 1 n k
105 fzfi 1 n 1 Fin
106 fprodconst 1 n 1 Fin n k = 1 n 1 n = n 1 n 1
107 105 50 106 sylancr n k = 1 n 1 n = n 1 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 n 1 n 1 = n n 1
111 107 110 eqtr2d n n n 1 = k = 1 n 1 n
112 fprodfac n 1 0 n 1 ! = j = 1 n 1 j
113 80 112 syl n n 1 ! = j = 1 n 1 j
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 = 1 n 1 j = k = n n 1 n 1 n 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 1 n 1 n k = k = 1 n 1 n k
125 113 121 124 3eqtrd n n 1 ! = k = 1 n 1 n k
126 111 125 oveq12d n n n 1 n 1 ! = k = 1 n 1 n k = 1 n 1 n k
127 104 126 eqtr4d n k = 1 n 1 n n k = n n 1 n 1 !
128 127 oveq2d n k = 1 n 1 ( n 1 k) k = 1 n 1 n n k = k = 1 n 1 ( n 1 k) n n 1 n 1 !
129 79 103 128 3eqtrd n k = 1 n 1 ( n k) = k = 1 n 1 ( n 1 k) n n 1 n 1 !
130 68 74 129 3eqtrd n k = 1 n 1 ( n k) ( n n) = k = 1 n 1 ( n 1 k) n n 1 n 1 !
131 56 65 130 3eqtrd n k = 1 n + 1 - 1 ( n + 1 - 1 k) = k = 1 n 1 ( n 1 k) n n 1 n 1 !
132 131 adantr n k = 1 n 1 ( n 1 k) = k = 1 n 1 k 2 k n k = 1 n + 1 - 1 ( n + 1 - 1 k) = k = 1 n 1 ( n 1 k) n n 1 n 1 !
133 53 prodeq1d n k = 1 n + 1 - 1 k 2 k n + 1 = k = 1 n k 2 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 k 2 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 k 2 k n + 1 = n 2 n n + 1
151 58 146 150 fprodm1 n k = 1 n k 2 k n + 1 = k = 1 n 1 k 2 k n + 1 n 2 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 k 2 k n
160 69 159 152 153 fproddiv n k = 1 n 1 k 2 k n k = k = 1 n 1 k 2 k n k = 1 n 1 k
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 k 2 k - n - 1 = k 2 k n + 1
165 152 153 158 expm1d n k 1 n 1 k 2 k - n - 1 = k 2 k n k
166 164 165 eqtr3d n k 1 n 1 k 2 k n + 1 = k 2 k n k
167 166 prodeq2dv n k = 1 n 1 k 2 k n + 1 = k = 1 n 1 k 2 k n k
168 fprodfac n 1 0 n 1 ! = k = 1 n 1 k
169 80 168 syl n n 1 ! = k = 1 n 1 k
170 169 oveq2d n k = 1 n 1 k 2 k n n 1 ! = k = 1 n 1 k 2 k n k = 1 n 1 k
171 160 167 170 3eqtr4d n k = 1 n 1 k 2 k n + 1 = k = 1 n 1 k 2 k n n 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 n 2 n n + 1 = n n 1
182 171 181 oveq12d n k = 1 n 1 k 2 k n + 1 n 2 n n + 1 = k = 1 n 1 k 2 k n n 1 ! n n 1
183 69 159 fprodcl n k = 1 n 1 k 2 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 n n 1
188 185 nnne0d n n 1 ! 0
189 183 186 187 188 div32d n k = 1 n 1 k 2 k n n 1 ! n n 1 = k = 1 n 1 k 2 k n n n 1 n 1 !
190 182 189 eqtrd n k = 1 n 1 k 2 k n + 1 n 2 n n + 1 = k = 1 n 1 k 2 k n n n 1 n 1 !
191 133 151 190 3eqtrd n k = 1 n + 1 - 1 k 2 k n + 1 = k = 1 n 1 k 2 k n n n 1 n 1 !
192 191 adantr n k = 1 n 1 ( n 1 k) = k = 1 n 1 k 2 k n k = 1 n + 1 - 1 k 2 k n + 1 = k = 1 n 1 k 2 k n n n 1 n 1 !
193 49 132 192 3eqtr4d n k = 1 n 1 ( n 1 k) = k = 1 n 1 k 2 k n k = 1 n + 1 - 1 ( n + 1 - 1 k) = k = 1 n + 1 - 1 k 2 k n + 1
194 193 ex n k = 1 n 1 ( n 1 k) = k = 1 n 1 k 2 k n k = 1 n + 1 - 1 ( n + 1 - 1 k) = k = 1 n + 1 - 1 k 2 k n + 1
195 14 24 34 44 47 194 nnind N k = 1 N 1 ( N 1 k) = k = 1 N 1 k 2 k N