Metamath Proof Explorer

Theorem bcprod

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

Ref Expression
Assertion bcprod ( 𝑁 ∈ ℕ → ∏ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( ( 𝑁 − 1 ) C 𝑘 ) = ∏ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 𝑘 ↑ ( ( 2 · 𝑘 ) − 𝑁 ) ) )

Proof

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