Step | Hyp | Ref
| Expression |
1 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1)) |
2 | | 1m1e0 12045 |
. . . . . . 7
⊢ (1
− 1) = 0 |
3 | 1, 2 | eqtrdi 2794 |
. . . . . 6
⊢ (𝑚 = 1 → (𝑚 − 1) = 0) |
4 | 3 | oveq2d 7291 |
. . . . 5
⊢ (𝑚 = 1 → (1...(𝑚 − 1)) =
(1...0)) |
5 | | fz10 13277 |
. . . . 5
⊢ (1...0) =
∅ |
6 | 4, 5 | eqtrdi 2794 |
. . . 4
⊢ (𝑚 = 1 → (1...(𝑚 − 1)) =
∅) |
7 | 3 | oveq1d 7290 |
. . . . 5
⊢ (𝑚 = 1 → ((𝑚 − 1)C𝑘) = (0C𝑘)) |
8 | 7 | adantr 481 |
. . . 4
⊢ ((𝑚 = 1 ∧ 𝑘 ∈ (1...(𝑚 − 1))) → ((𝑚 − 1)C𝑘) = (0C𝑘)) |
9 | 6, 8 | prodeq12dv 15636 |
. . 3
⊢ (𝑚 = 1 → ∏𝑘 ∈ (1...(𝑚 − 1))((𝑚 − 1)C𝑘) = ∏𝑘 ∈ ∅ (0C𝑘)) |
10 | | oveq2 7283 |
. . . . . 6
⊢ (𝑚 = 1 → ((2 · 𝑘) − 𝑚) = ((2 · 𝑘) − 1)) |
11 | 10 | oveq2d 7291 |
. . . . 5
⊢ (𝑚 = 1 → (𝑘↑((2 · 𝑘) − 𝑚)) = (𝑘↑((2 · 𝑘) − 1))) |
12 | 11 | adantr 481 |
. . . 4
⊢ ((𝑚 = 1 ∧ 𝑘 ∈ (1...(𝑚 − 1))) → (𝑘↑((2 · 𝑘) − 𝑚)) = (𝑘↑((2 · 𝑘) − 1))) |
13 | 6, 12 | prodeq12dv 15636 |
. . 3
⊢ (𝑚 = 1 → ∏𝑘 ∈ (1...(𝑚 − 1))(𝑘↑((2 · 𝑘) − 𝑚)) = ∏𝑘 ∈ ∅ (𝑘↑((2 · 𝑘) − 1))) |
14 | 9, 13 | eqeq12d 2754 |
. 2
⊢ (𝑚 = 1 → (∏𝑘 ∈ (1...(𝑚 − 1))((𝑚 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑚 − 1))(𝑘↑((2 · 𝑘) − 𝑚)) ↔ ∏𝑘 ∈ ∅ (0C𝑘) = ∏𝑘 ∈ ∅ (𝑘↑((2 · 𝑘) − 1)))) |
15 | | oveq1 7282 |
. . . . 5
⊢ (𝑚 = 𝑛 → (𝑚 − 1) = (𝑛 − 1)) |
16 | 15 | oveq2d 7291 |
. . . 4
⊢ (𝑚 = 𝑛 → (1...(𝑚 − 1)) = (1...(𝑛 − 1))) |
17 | 15 | oveq1d 7290 |
. . . . 5
⊢ (𝑚 = 𝑛 → ((𝑚 − 1)C𝑘) = ((𝑛 − 1)C𝑘)) |
18 | 17 | adantr 481 |
. . . 4
⊢ ((𝑚 = 𝑛 ∧ 𝑘 ∈ (1...(𝑚 − 1))) → ((𝑚 − 1)C𝑘) = ((𝑛 − 1)C𝑘)) |
19 | 16, 18 | prodeq12dv 15636 |
. . 3
⊢ (𝑚 = 𝑛 → ∏𝑘 ∈ (1...(𝑚 − 1))((𝑚 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑛 − 1))((𝑛 − 1)C𝑘)) |
20 | | oveq2 7283 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((2 · 𝑘) − 𝑚) = ((2 · 𝑘) − 𝑛)) |
21 | 20 | oveq2d 7291 |
. . . . 5
⊢ (𝑚 = 𝑛 → (𝑘↑((2 · 𝑘) − 𝑚)) = (𝑘↑((2 · 𝑘) − 𝑛))) |
22 | 21 | adantr 481 |
. . . 4
⊢ ((𝑚 = 𝑛 ∧ 𝑘 ∈ (1...(𝑚 − 1))) → (𝑘↑((2 · 𝑘) − 𝑚)) = (𝑘↑((2 · 𝑘) − 𝑛))) |
23 | 16, 22 | prodeq12dv 15636 |
. . 3
⊢ (𝑚 = 𝑛 → ∏𝑘 ∈ (1...(𝑚 − 1))(𝑘↑((2 · 𝑘) − 𝑚)) = ∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛))) |
24 | 19, 23 | eqeq12d 2754 |
. 2
⊢ (𝑚 = 𝑛 → (∏𝑘 ∈ (1...(𝑚 − 1))((𝑚 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑚 − 1))(𝑘↑((2 · 𝑘) − 𝑚)) ↔ ∏𝑘 ∈ (1...(𝑛 − 1))((𝑛 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛)))) |
25 | | oveq1 7282 |
. . . . 5
⊢ (𝑚 = (𝑛 + 1) → (𝑚 − 1) = ((𝑛 + 1) − 1)) |
26 | 25 | oveq2d 7291 |
. . . 4
⊢ (𝑚 = (𝑛 + 1) → (1...(𝑚 − 1)) = (1...((𝑛 + 1) − 1))) |
27 | 25 | oveq1d 7290 |
. . . . 5
⊢ (𝑚 = (𝑛 + 1) → ((𝑚 − 1)C𝑘) = (((𝑛 + 1) − 1)C𝑘)) |
28 | 27 | adantr 481 |
. . . 4
⊢ ((𝑚 = (𝑛 + 1) ∧ 𝑘 ∈ (1...(𝑚 − 1))) → ((𝑚 − 1)C𝑘) = (((𝑛 + 1) − 1)C𝑘)) |
29 | 26, 28 | prodeq12dv 15636 |
. . 3
⊢ (𝑚 = (𝑛 + 1) → ∏𝑘 ∈ (1...(𝑚 − 1))((𝑚 − 1)C𝑘) = ∏𝑘 ∈ (1...((𝑛 + 1) − 1))(((𝑛 + 1) − 1)C𝑘)) |
30 | | oveq2 7283 |
. . . . . 6
⊢ (𝑚 = (𝑛 + 1) → ((2 · 𝑘) − 𝑚) = ((2 · 𝑘) − (𝑛 + 1))) |
31 | 30 | oveq2d 7291 |
. . . . 5
⊢ (𝑚 = (𝑛 + 1) → (𝑘↑((2 · 𝑘) − 𝑚)) = (𝑘↑((2 · 𝑘) − (𝑛 + 1)))) |
32 | 31 | adantr 481 |
. . . 4
⊢ ((𝑚 = (𝑛 + 1) ∧ 𝑘 ∈ (1...(𝑚 − 1))) → (𝑘↑((2 · 𝑘) − 𝑚)) = (𝑘↑((2 · 𝑘) − (𝑛 + 1)))) |
33 | 26, 32 | prodeq12dv 15636 |
. . 3
⊢ (𝑚 = (𝑛 + 1) → ∏𝑘 ∈ (1...(𝑚 − 1))(𝑘↑((2 · 𝑘) − 𝑚)) = ∏𝑘 ∈ (1...((𝑛 + 1) − 1))(𝑘↑((2 · 𝑘) − (𝑛 + 1)))) |
34 | 29, 33 | eqeq12d 2754 |
. 2
⊢ (𝑚 = (𝑛 + 1) → (∏𝑘 ∈ (1...(𝑚 − 1))((𝑚 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑚 − 1))(𝑘↑((2 · 𝑘) − 𝑚)) ↔ ∏𝑘 ∈ (1...((𝑛 + 1) − 1))(((𝑛 + 1) − 1)C𝑘) = ∏𝑘 ∈ (1...((𝑛 + 1) − 1))(𝑘↑((2 · 𝑘) − (𝑛 + 1))))) |
35 | | oveq1 7282 |
. . . . 5
⊢ (𝑚 = 𝑁 → (𝑚 − 1) = (𝑁 − 1)) |
36 | 35 | oveq2d 7291 |
. . . 4
⊢ (𝑚 = 𝑁 → (1...(𝑚 − 1)) = (1...(𝑁 − 1))) |
37 | 35 | oveq1d 7290 |
. . . . 5
⊢ (𝑚 = 𝑁 → ((𝑚 − 1)C𝑘) = ((𝑁 − 1)C𝑘)) |
38 | 37 | adantr 481 |
. . . 4
⊢ ((𝑚 = 𝑁 ∧ 𝑘 ∈ (1...(𝑚 − 1))) → ((𝑚 − 1)C𝑘) = ((𝑁 − 1)C𝑘)) |
39 | 36, 38 | prodeq12dv 15636 |
. . 3
⊢ (𝑚 = 𝑁 → ∏𝑘 ∈ (1...(𝑚 − 1))((𝑚 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑁 − 1))((𝑁 − 1)C𝑘)) |
40 | | oveq2 7283 |
. . . . . 6
⊢ (𝑚 = 𝑁 → ((2 · 𝑘) − 𝑚) = ((2 · 𝑘) − 𝑁)) |
41 | 40 | oveq2d 7291 |
. . . . 5
⊢ (𝑚 = 𝑁 → (𝑘↑((2 · 𝑘) − 𝑚)) = (𝑘↑((2 · 𝑘) − 𝑁))) |
42 | 41 | adantr 481 |
. . . 4
⊢ ((𝑚 = 𝑁 ∧ 𝑘 ∈ (1...(𝑚 − 1))) → (𝑘↑((2 · 𝑘) − 𝑚)) = (𝑘↑((2 · 𝑘) − 𝑁))) |
43 | 36, 42 | prodeq12dv 15636 |
. . 3
⊢ (𝑚 = 𝑁 → ∏𝑘 ∈ (1...(𝑚 − 1))(𝑘↑((2 · 𝑘) − 𝑚)) = ∏𝑘 ∈ (1...(𝑁 − 1))(𝑘↑((2 · 𝑘) − 𝑁))) |
44 | 39, 43 | eqeq12d 2754 |
. 2
⊢ (𝑚 = 𝑁 → (∏𝑘 ∈ (1...(𝑚 − 1))((𝑚 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑚 − 1))(𝑘↑((2 · 𝑘) − 𝑚)) ↔ ∏𝑘 ∈ (1...(𝑁 − 1))((𝑁 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑁 − 1))(𝑘↑((2 · 𝑘) − 𝑁)))) |
45 | | prod0 15653 |
. . 3
⊢
∏𝑘 ∈
∅ (0C𝑘) =
1 |
46 | | prod0 15653 |
. . 3
⊢
∏𝑘 ∈
∅ (𝑘↑((2
· 𝑘) − 1)) =
1 |
47 | 45, 46 | eqtr4i 2769 |
. 2
⊢
∏𝑘 ∈
∅ (0C𝑘) =
∏𝑘 ∈ ∅
(𝑘↑((2 · 𝑘) − 1)) |
48 | | simpr 485 |
. . . . 5
⊢ ((𝑛 ∈ ℕ ∧
∏𝑘 ∈ (1...(𝑛 − 1))((𝑛 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛))) → ∏𝑘 ∈ (1...(𝑛 − 1))((𝑛 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛))) |
49 | 48 | oveq1d 7290 |
. . . 4
⊢ ((𝑛 ∈ ℕ ∧
∏𝑘 ∈ (1...(𝑛 − 1))((𝑛 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛))) → (∏𝑘 ∈ (1...(𝑛 − 1))((𝑛 − 1)C𝑘) · ((𝑛↑(𝑛 − 1)) / (!‘(𝑛 − 1)))) = (∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛)) · ((𝑛↑(𝑛 − 1)) / (!‘(𝑛 − 1))))) |
50 | | nncn 11981 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
51 | | 1cnd 10970 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 1 ∈
ℂ) |
52 | 50, 51 | pncand 11333 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ((𝑛 + 1) − 1) = 𝑛) |
53 | 52 | oveq2d 7291 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
(1...((𝑛 + 1) − 1)) =
(1...𝑛)) |
54 | 52 | oveq1d 7290 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (((𝑛 + 1) − 1)C𝑘) = (𝑛C𝑘)) |
55 | 54 | adantr 481 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...((𝑛 + 1) − 1))) →
(((𝑛 + 1) − 1)C𝑘) = (𝑛C𝑘)) |
56 | 53, 55 | prodeq12dv 15636 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈
(1...((𝑛 + 1) −
1))(((𝑛 + 1) −
1)C𝑘) = ∏𝑘 ∈ (1...𝑛)(𝑛C𝑘)) |
57 | | elnnuz 12622 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘1)) |
58 | 57 | biimpi 215 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
(ℤ≥‘1)) |
59 | | nnnn0 12240 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
60 | | elfzelz 13256 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℤ) |
61 | | bccl 14036 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑛C𝑘) ∈
ℕ0) |
62 | 59, 60, 61 | syl2an 596 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...𝑛)) → (𝑛C𝑘) ∈
ℕ0) |
63 | 62 | nn0cnd 12295 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...𝑛)) → (𝑛C𝑘) ∈ ℂ) |
64 | | oveq2 7283 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (𝑛C𝑘) = (𝑛C𝑛)) |
65 | 58, 63, 64 | fprodm1 15677 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈ (1...𝑛)(𝑛C𝑘) = (∏𝑘 ∈ (1...(𝑛 − 1))(𝑛C𝑘) · (𝑛C𝑛))) |
66 | | bcnn 14026 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ (𝑛C𝑛) = 1) |
67 | 59, 66 | syl 17 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝑛C𝑛) = 1) |
68 | 67 | oveq2d 7291 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
(∏𝑘 ∈
(1...(𝑛 − 1))(𝑛C𝑘) · (𝑛C𝑛)) = (∏𝑘 ∈ (1...(𝑛 − 1))(𝑛C𝑘) · 1)) |
69 | | fzfid 13693 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(1...(𝑛 − 1)) ∈
Fin) |
70 | | elfzelz 13256 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...(𝑛 − 1)) → 𝑘 ∈ ℤ) |
71 | 59, 70, 61 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (𝑛C𝑘) ∈
ℕ0) |
72 | 71 | nn0cnd 12295 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (𝑛C𝑘) ∈ ℂ) |
73 | 69, 72 | fprodcl 15662 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈ (1...(𝑛 − 1))(𝑛C𝑘) ∈ ℂ) |
74 | 73 | mulid1d 10992 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
(∏𝑘 ∈
(1...(𝑛 − 1))(𝑛C𝑘) · 1) = ∏𝑘 ∈ (1...(𝑛 − 1))(𝑛C𝑘)) |
75 | | fz1ssfz0 13352 |
. . . . . . . . . . 11
⊢
(1...(𝑛 − 1))
⊆ (0...(𝑛 −
1)) |
76 | 75 | sseli 3917 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...(𝑛 − 1)) → 𝑘 ∈ (0...(𝑛 − 1))) |
77 | | bcm1nt 33703 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (0...(𝑛 − 1))) → (𝑛C𝑘) = (((𝑛 − 1)C𝑘) · (𝑛 / (𝑛 − 𝑘)))) |
78 | 76, 77 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (𝑛C𝑘) = (((𝑛 − 1)C𝑘) · (𝑛 / (𝑛 − 𝑘)))) |
79 | 78 | prodeq2dv 15633 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈ (1...(𝑛 − 1))(𝑛C𝑘) = ∏𝑘 ∈ (1...(𝑛 − 1))(((𝑛 − 1)C𝑘) · (𝑛 / (𝑛 − 𝑘)))) |
80 | | nnm1nn0 12274 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
81 | | bccl 14036 |
. . . . . . . . . . 11
⊢ (((𝑛 − 1) ∈
ℕ0 ∧ 𝑘
∈ ℤ) → ((𝑛
− 1)C𝑘) ∈
ℕ0) |
82 | 80, 70, 81 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → ((𝑛 − 1)C𝑘) ∈
ℕ0) |
83 | 82 | nn0cnd 12295 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → ((𝑛 − 1)C𝑘) ∈ ℂ) |
84 | 50 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → 𝑛 ∈ ℂ) |
85 | | elfznn 13285 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (1...(𝑛 − 1)) → 𝑘 ∈ ℕ) |
86 | 85 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → 𝑘 ∈ ℕ) |
87 | 86 | nnred 11988 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → 𝑘 ∈ ℝ) |
88 | 80 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (𝑛 − 1) ∈
ℕ0) |
89 | 88 | nn0red 12294 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (𝑛 − 1) ∈ ℝ) |
90 | | nnre 11980 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
91 | 90 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → 𝑛 ∈ ℝ) |
92 | | elfzle2 13260 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1...(𝑛 − 1)) → 𝑘 ≤ (𝑛 − 1)) |
93 | 92 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → 𝑘 ≤ (𝑛 − 1)) |
94 | 91 | ltm1d 11907 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (𝑛 − 1) < 𝑛) |
95 | 87, 89, 91, 93, 94 | lelttrd 11133 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → 𝑘 < 𝑛) |
96 | | simpl 483 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → 𝑛 ∈ ℕ) |
97 | | nnsub 12017 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑘 < 𝑛 ↔ (𝑛 − 𝑘) ∈ ℕ)) |
98 | 86, 96, 97 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (𝑘 < 𝑛 ↔ (𝑛 − 𝑘) ∈ ℕ)) |
99 | 95, 98 | mpbid 231 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (𝑛 − 𝑘) ∈ ℕ) |
100 | 99 | nncnd 11989 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (𝑛 − 𝑘) ∈ ℂ) |
101 | 99 | nnne0d 12023 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (𝑛 − 𝑘) ≠ 0) |
102 | 84, 100, 101 | divcld 11751 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (𝑛 / (𝑛 − 𝑘)) ∈ ℂ) |
103 | 69, 83, 102 | fprodmul 15670 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈ (1...(𝑛 − 1))(((𝑛 − 1)C𝑘) · (𝑛 / (𝑛 − 𝑘))) = (∏𝑘 ∈ (1...(𝑛 − 1))((𝑛 − 1)C𝑘) · ∏𝑘 ∈ (1...(𝑛 − 1))(𝑛 / (𝑛 − 𝑘)))) |
104 | 69, 84, 100, 101 | fproddiv 15671 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈ (1...(𝑛 − 1))(𝑛 / (𝑛 − 𝑘)) = (∏𝑘 ∈ (1...(𝑛 − 1))𝑛 / ∏𝑘 ∈ (1...(𝑛 − 1))(𝑛 − 𝑘))) |
105 | | fzfi 13692 |
. . . . . . . . . . . . 13
⊢
(1...(𝑛 − 1))
∈ Fin |
106 | | fprodconst 15688 |
. . . . . . . . . . . . 13
⊢
(((1...(𝑛 −
1)) ∈ Fin ∧ 𝑛
∈ ℂ) → ∏𝑘 ∈ (1...(𝑛 − 1))𝑛 = (𝑛↑(♯‘(1...(𝑛 − 1))))) |
107 | 105, 50, 106 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈ (1...(𝑛 − 1))𝑛 = (𝑛↑(♯‘(1...(𝑛 − 1))))) |
108 | | hashfz1 14060 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 − 1) ∈
ℕ0 → (♯‘(1...(𝑛 − 1))) = (𝑛 − 1)) |
109 | 80, 108 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(♯‘(1...(𝑛
− 1))) = (𝑛 −
1)) |
110 | 109 | oveq2d 7291 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛↑(♯‘(1...(𝑛 − 1)))) = (𝑛↑(𝑛 − 1))) |
111 | 107, 110 | eqtr2d 2779 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (𝑛↑(𝑛 − 1)) = ∏𝑘 ∈ (1...(𝑛 − 1))𝑛) |
112 | | fprodfac 15683 |
. . . . . . . . . . . . 13
⊢ ((𝑛 − 1) ∈
ℕ0 → (!‘(𝑛 − 1)) = ∏𝑗 ∈ (1...(𝑛 − 1))𝑗) |
113 | 80, 112 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
(!‘(𝑛 − 1)) =
∏𝑗 ∈ (1...(𝑛 − 1))𝑗) |
114 | | nnz 12342 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
115 | | 1zzd 12351 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 1 ∈
ℤ) |
116 | 80 | nn0zd 12424 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℤ) |
117 | | elfznn 13285 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (1...(𝑛 − 1)) → 𝑗 ∈ ℕ) |
118 | 117 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑛 − 1))) → 𝑗 ∈ ℕ) |
119 | 118 | nncnd 11989 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑛 − 1))) → 𝑗 ∈ ℂ) |
120 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑛 − 𝑘) → 𝑗 = (𝑛 − 𝑘)) |
121 | 114, 115,
116, 119, 120 | fprodrev 15687 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
∏𝑗 ∈ (1...(𝑛 − 1))𝑗 = ∏𝑘 ∈ ((𝑛 − (𝑛 − 1))...(𝑛 − 1))(𝑛 − 𝑘)) |
122 | 50, 51 | nncand 11337 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (𝑛 − (𝑛 − 1)) = 1) |
123 | 122 | oveq1d 7290 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → ((𝑛 − (𝑛 − 1))...(𝑛 − 1)) = (1...(𝑛 − 1))) |
124 | 123 | prodeq1d 15631 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈ ((𝑛 − (𝑛 − 1))...(𝑛 − 1))(𝑛 − 𝑘) = ∏𝑘 ∈ (1...(𝑛 − 1))(𝑛 − 𝑘)) |
125 | 113, 121,
124 | 3eqtrd 2782 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(!‘(𝑛 − 1)) =
∏𝑘 ∈ (1...(𝑛 − 1))(𝑛 − 𝑘)) |
126 | 111, 125 | oveq12d 7293 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → ((𝑛↑(𝑛 − 1)) / (!‘(𝑛 − 1))) = (∏𝑘 ∈ (1...(𝑛 − 1))𝑛 / ∏𝑘 ∈ (1...(𝑛 − 1))(𝑛 − 𝑘))) |
127 | 104, 126 | eqtr4d 2781 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈ (1...(𝑛 − 1))(𝑛 / (𝑛 − 𝑘)) = ((𝑛↑(𝑛 − 1)) / (!‘(𝑛 − 1)))) |
128 | 127 | oveq2d 7291 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(∏𝑘 ∈
(1...(𝑛 − 1))((𝑛 − 1)C𝑘) · ∏𝑘 ∈ (1...(𝑛 − 1))(𝑛 / (𝑛 − 𝑘))) = (∏𝑘 ∈ (1...(𝑛 − 1))((𝑛 − 1)C𝑘) · ((𝑛↑(𝑛 − 1)) / (!‘(𝑛 − 1))))) |
129 | 79, 103, 128 | 3eqtrd 2782 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈ (1...(𝑛 − 1))(𝑛C𝑘) = (∏𝑘 ∈ (1...(𝑛 − 1))((𝑛 − 1)C𝑘) · ((𝑛↑(𝑛 − 1)) / (!‘(𝑛 − 1))))) |
130 | 68, 74, 129 | 3eqtrd 2782 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
(∏𝑘 ∈
(1...(𝑛 − 1))(𝑛C𝑘) · (𝑛C𝑛)) = (∏𝑘 ∈ (1...(𝑛 − 1))((𝑛 − 1)C𝑘) · ((𝑛↑(𝑛 − 1)) / (!‘(𝑛 − 1))))) |
131 | 56, 65, 130 | 3eqtrd 2782 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈
(1...((𝑛 + 1) −
1))(((𝑛 + 1) −
1)C𝑘) = (∏𝑘 ∈ (1...(𝑛 − 1))((𝑛 − 1)C𝑘) · ((𝑛↑(𝑛 − 1)) / (!‘(𝑛 − 1))))) |
132 | 131 | adantr 481 |
. . . 4
⊢ ((𝑛 ∈ ℕ ∧
∏𝑘 ∈ (1...(𝑛 − 1))((𝑛 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛))) → ∏𝑘 ∈ (1...((𝑛 + 1) − 1))(((𝑛 + 1) − 1)C𝑘) = (∏𝑘 ∈ (1...(𝑛 − 1))((𝑛 − 1)C𝑘) · ((𝑛↑(𝑛 − 1)) / (!‘(𝑛 − 1))))) |
133 | 53 | prodeq1d 15631 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈
(1...((𝑛 + 1) −
1))(𝑘↑((2 ·
𝑘) − (𝑛 + 1))) = ∏𝑘 ∈ (1...𝑛)(𝑘↑((2 · 𝑘) − (𝑛 + 1)))) |
134 | | elfznn 13285 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ) |
135 | 134 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
136 | 135 | nncnd 11989 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℂ) |
137 | 135 | nnne0d 12023 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ≠ 0) |
138 | | 2nn 12046 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
139 | 138 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...𝑛)) → 2 ∈ ℕ) |
140 | 139, 135 | nnmulcld 12026 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...𝑛)) → (2 · 𝑘) ∈ ℕ) |
141 | 140 | nnzd 12425 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...𝑛)) → (2 · 𝑘) ∈ ℤ) |
142 | | peano2nn 11985 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
143 | 142 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...𝑛)) → (𝑛 + 1) ∈ ℕ) |
144 | 143 | nnzd 12425 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...𝑛)) → (𝑛 + 1) ∈ ℤ) |
145 | 141, 144 | zsubcld 12431 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...𝑛)) → ((2 · 𝑘) − (𝑛 + 1)) ∈ ℤ) |
146 | 136, 137,
145 | expclzd 13869 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...𝑛)) → (𝑘↑((2 · 𝑘) − (𝑛 + 1))) ∈ ℂ) |
147 | | id 22 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → 𝑘 = 𝑛) |
148 | | oveq2 7283 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛)) |
149 | 148 | oveq1d 7290 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((2 · 𝑘) − (𝑛 + 1)) = ((2 · 𝑛) − (𝑛 + 1))) |
150 | 147, 149 | oveq12d 7293 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (𝑘↑((2 · 𝑘) − (𝑛 + 1))) = (𝑛↑((2 · 𝑛) − (𝑛 + 1)))) |
151 | 58, 146, 150 | fprodm1 15677 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈ (1...𝑛)(𝑘↑((2 · 𝑘) − (𝑛 + 1))) = (∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − (𝑛 + 1))) · (𝑛↑((2 · 𝑛) − (𝑛 + 1))))) |
152 | 86 | nncnd 11989 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → 𝑘 ∈ ℂ) |
153 | 86 | nnne0d 12023 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → 𝑘 ≠ 0) |
154 | 138 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → 2 ∈
ℕ) |
155 | 154, 86 | nnmulcld 12026 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (2 · 𝑘) ∈
ℕ) |
156 | 155 | nnzd 12425 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (2 · 𝑘) ∈
ℤ) |
157 | 114 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → 𝑛 ∈ ℤ) |
158 | 156, 157 | zsubcld 12431 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → ((2 · 𝑘) − 𝑛) ∈ ℤ) |
159 | 152, 153,
158 | expclzd 13869 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (𝑘↑((2 · 𝑘) − 𝑛)) ∈ ℂ) |
160 | 69, 159, 152, 153 | fproddiv 15671 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈ (1...(𝑛 − 1))((𝑘↑((2 · 𝑘) − 𝑛)) / 𝑘) = (∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛)) / ∏𝑘 ∈ (1...(𝑛 − 1))𝑘)) |
161 | 155 | nncnd 11989 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (2 · 𝑘) ∈
ℂ) |
162 | | 1cnd 10970 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → 1 ∈
ℂ) |
163 | 161, 84, 162 | subsub4d 11363 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (((2 · 𝑘) − 𝑛) − 1) = ((2 · 𝑘) − (𝑛 + 1))) |
164 | 163 | oveq2d 7291 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (𝑘↑(((2 · 𝑘) − 𝑛) − 1)) = (𝑘↑((2 · 𝑘) − (𝑛 + 1)))) |
165 | 152, 153,
158 | expm1d 13874 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (𝑘↑(((2 · 𝑘) − 𝑛) − 1)) = ((𝑘↑((2 · 𝑘) − 𝑛)) / 𝑘)) |
166 | 164, 165 | eqtr3d 2780 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑛 − 1))) → (𝑘↑((2 · 𝑘) − (𝑛 + 1))) = ((𝑘↑((2 · 𝑘) − 𝑛)) / 𝑘)) |
167 | 166 | prodeq2dv 15633 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − (𝑛 + 1))) = ∏𝑘 ∈ (1...(𝑛 − 1))((𝑘↑((2 · 𝑘) − 𝑛)) / 𝑘)) |
168 | | fprodfac 15683 |
. . . . . . . . . . 11
⊢ ((𝑛 − 1) ∈
ℕ0 → (!‘(𝑛 − 1)) = ∏𝑘 ∈ (1...(𝑛 − 1))𝑘) |
169 | 80, 168 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(!‘(𝑛 − 1)) =
∏𝑘 ∈ (1...(𝑛 − 1))𝑘) |
170 | 169 | oveq2d 7291 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(∏𝑘 ∈
(1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛)) / (!‘(𝑛 − 1))) = (∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛)) / ∏𝑘 ∈ (1...(𝑛 − 1))𝑘)) |
171 | 160, 167,
170 | 3eqtr4d 2788 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − (𝑛 + 1))) = (∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛)) / (!‘(𝑛 − 1)))) |
172 | 138 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 2 ∈
ℕ) |
173 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ) |
174 | 172, 173 | nnmulcld 12026 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℕ) |
175 | 174 | nncnd 11989 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) ∈
ℂ) |
176 | 175, 50, 51 | subsub4d 11363 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛) − 𝑛) − 1) = ((2 ·
𝑛) − (𝑛 + 1))) |
177 | 50 | 2timesd 12216 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (2
· 𝑛) = (𝑛 + 𝑛)) |
178 | 50, 50, 177 | mvrladdd 11388 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) − 𝑛) = 𝑛) |
179 | 178 | oveq1d 7290 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (((2
· 𝑛) − 𝑛) − 1) = (𝑛 − 1)) |
180 | 176, 179 | eqtr3d 2780 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((2
· 𝑛) − (𝑛 + 1)) = (𝑛 − 1)) |
181 | 180 | oveq2d 7291 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝑛↑((2 · 𝑛) − (𝑛 + 1))) = (𝑛↑(𝑛 − 1))) |
182 | 171, 181 | oveq12d 7293 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
(∏𝑘 ∈
(1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − (𝑛 + 1))) · (𝑛↑((2 · 𝑛) − (𝑛 + 1)))) = ((∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛)) / (!‘(𝑛 − 1))) · (𝑛↑(𝑛 − 1)))) |
183 | 69, 159 | fprodcl 15662 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛)) ∈ ℂ) |
184 | | faccl 13997 |
. . . . . . . . . 10
⊢ ((𝑛 − 1) ∈
ℕ0 → (!‘(𝑛 − 1)) ∈ ℕ) |
185 | 80, 184 | syl 17 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(!‘(𝑛 − 1))
∈ ℕ) |
186 | 185 | nncnd 11989 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(!‘(𝑛 − 1))
∈ ℂ) |
187 | 50, 80 | expcld 13864 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝑛↑(𝑛 − 1)) ∈ ℂ) |
188 | 185 | nnne0d 12023 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(!‘(𝑛 − 1))
≠ 0) |
189 | 183, 186,
187, 188 | div32d 11774 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
((∏𝑘 ∈
(1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛)) / (!‘(𝑛 − 1))) · (𝑛↑(𝑛 − 1))) = (∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛)) · ((𝑛↑(𝑛 − 1)) / (!‘(𝑛 − 1))))) |
190 | 182, 189 | eqtrd 2778 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
(∏𝑘 ∈
(1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − (𝑛 + 1))) · (𝑛↑((2 · 𝑛) − (𝑛 + 1)))) = (∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛)) · ((𝑛↑(𝑛 − 1)) / (!‘(𝑛 − 1))))) |
191 | 133, 151,
190 | 3eqtrd 2782 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈
(1...((𝑛 + 1) −
1))(𝑘↑((2 ·
𝑘) − (𝑛 + 1))) = (∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛)) · ((𝑛↑(𝑛 − 1)) / (!‘(𝑛 − 1))))) |
192 | 191 | adantr 481 |
. . . 4
⊢ ((𝑛 ∈ ℕ ∧
∏𝑘 ∈ (1...(𝑛 − 1))((𝑛 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛))) → ∏𝑘 ∈ (1...((𝑛 + 1) − 1))(𝑘↑((2 · 𝑘) − (𝑛 + 1))) = (∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛)) · ((𝑛↑(𝑛 − 1)) / (!‘(𝑛 − 1))))) |
193 | 49, 132, 192 | 3eqtr4d 2788 |
. . 3
⊢ ((𝑛 ∈ ℕ ∧
∏𝑘 ∈ (1...(𝑛 − 1))((𝑛 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑛 − 1))(𝑘↑((2 · 𝑘) − 𝑛))) → ∏𝑘 ∈ (1...((𝑛 + 1) − 1))(((𝑛 + 1) − 1)C𝑘) = ∏𝑘 ∈ (1...((𝑛 + 1) − 1))(𝑘↑((2 · 𝑘) − (𝑛 + 1)))) |
194 | 193 | ex 413 |
. 2
⊢ (𝑛 ∈ ℕ →
(∏𝑘 ∈
(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 11991 |
1
⊢ (𝑁 ∈ ℕ →
∏𝑘 ∈ (1...(𝑁 − 1))((𝑁 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑁 − 1))(𝑘↑((2 · 𝑘) − 𝑁))) |