Metamath Proof Explorer

Theorem bcprod

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

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