Proof of Theorem bcm1k
Step | Hyp | Ref
| Expression |
1 | | elfzuz2 12600 |
. . . . . . . . 9
⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈
(ℤ≥‘1)) |
2 | | nnuz 11967 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
3 | 1, 2 | syl6eleqr 2889 |
. . . . . . . 8
⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ ℕ) |
4 | 3 | nnnn0d 11640 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈
ℕ0) |
5 | | faccl 13323 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → (!‘𝑁) ∈ ℕ) |
7 | 6 | nncnd 11330 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → (!‘𝑁) ∈ ℂ) |
8 | | fznn0sub 12627 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (𝑁 − 𝐾) ∈
ℕ0) |
9 | | nn0p1nn 11621 |
. . . . . . 7
⊢ ((𝑁 − 𝐾) ∈ ℕ0 → ((𝑁 − 𝐾) + 1) ∈ ℕ) |
10 | 8, 9 | syl 17 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − 𝐾) + 1) ∈ ℕ) |
11 | 10 | nncnd 11330 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − 𝐾) + 1) ∈ ℂ) |
12 | 10 | nnnn0d 11640 |
. . . . . . . 8
⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − 𝐾) + 1) ∈
ℕ0) |
13 | | faccl 13323 |
. . . . . . . 8
⊢ (((𝑁 − 𝐾) + 1) ∈ ℕ0 →
(!‘((𝑁 − 𝐾) + 1)) ∈
ℕ) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (!‘((𝑁 − 𝐾) + 1)) ∈ ℕ) |
15 | | elfznn 12624 |
. . . . . . . 8
⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ) |
16 | | nnm1nn0 11623 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈
ℕ0) |
17 | | faccl 13323 |
. . . . . . . 8
⊢ ((𝐾 − 1) ∈
ℕ0 → (!‘(𝐾 − 1)) ∈
ℕ) |
18 | 15, 16, 17 | 3syl 18 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (!‘(𝐾 − 1)) ∈
ℕ) |
19 | 14, 18 | nnmulcld 11366 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → ((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ∈
ℕ) |
20 | | nncn 11321 |
. . . . . . 7
⊢
(((!‘((𝑁
− 𝐾) + 1)) ·
(!‘(𝐾 − 1)))
∈ ℕ → ((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ∈
ℂ) |
21 | | nnne0 11348 |
. . . . . . 7
⊢
(((!‘((𝑁
− 𝐾) + 1)) ·
(!‘(𝐾 − 1)))
∈ ℕ → ((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ≠ 0) |
22 | 20, 21 | jca 508 |
. . . . . 6
⊢
(((!‘((𝑁
− 𝐾) + 1)) ·
(!‘(𝐾 − 1)))
∈ ℕ → (((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ∈ ℂ ∧
((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ≠
0)) |
23 | 19, 22 | syl 17 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → (((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ∈ ℂ ∧
((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ≠
0)) |
24 | 15 | nncnd 11330 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℂ) |
25 | 15 | nnne0d 11363 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ≠ 0) |
26 | 24, 25 | jca 508 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → (𝐾 ∈ ℂ ∧ 𝐾 ≠ 0)) |
27 | | divmuldiv 11017 |
. . . . 5
⊢
((((!‘𝑁)
∈ ℂ ∧ ((𝑁
− 𝐾) + 1) ∈
ℂ) ∧ ((((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ∈ ℂ ∧
((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ≠ 0) ∧
(𝐾 ∈ ℂ ∧
𝐾 ≠ 0))) →
(((!‘𝑁) /
((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1)))) · (((𝑁 − 𝐾) + 1) / 𝐾)) = (((!‘𝑁) · ((𝑁 − 𝐾) + 1)) / (((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) · 𝐾))) |
28 | 7, 11, 23, 26, 27 | syl22anc 868 |
. . . 4
⊢ (𝐾 ∈ (1...𝑁) → (((!‘𝑁) / ((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1)))) · (((𝑁 − 𝐾) + 1) / 𝐾)) = (((!‘𝑁) · ((𝑁 − 𝐾) + 1)) / (((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) · 𝐾))) |
29 | | elfzel2 12594 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ ℤ) |
30 | 29 | zcnd 11773 |
. . . . . . . . 9
⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ ℂ) |
31 | | 1cnd 10323 |
. . . . . . . . 9
⊢ (𝐾 ∈ (1...𝑁) → 1 ∈ ℂ) |
32 | 30, 24, 31 | subsubd 10712 |
. . . . . . . 8
⊢ (𝐾 ∈ (1...𝑁) → (𝑁 − (𝐾 − 1)) = ((𝑁 − 𝐾) + 1)) |
33 | 32 | fveq2d 6415 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (!‘(𝑁 − (𝐾 − 1))) = (!‘((𝑁 − 𝐾) + 1))) |
34 | 33 | oveq1d 6893 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → ((!‘(𝑁 − (𝐾 − 1))) · (!‘(𝐾 − 1))) =
((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1)))) |
35 | 34 | oveq2d 6894 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → ((!‘𝑁) / ((!‘(𝑁 − (𝐾 − 1))) · (!‘(𝐾 − 1)))) = ((!‘𝑁) / ((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))))) |
36 | 32 | oveq1d 6893 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − (𝐾 − 1)) / 𝐾) = (((𝑁 − 𝐾) + 1) / 𝐾)) |
37 | 35, 36 | oveq12d 6896 |
. . . 4
⊢ (𝐾 ∈ (1...𝑁) → (((!‘𝑁) / ((!‘(𝑁 − (𝐾 − 1))) · (!‘(𝐾 − 1)))) · ((𝑁 − (𝐾 − 1)) / 𝐾)) = (((!‘𝑁) / ((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1)))) · (((𝑁 − 𝐾) + 1) / 𝐾))) |
38 | | facp1 13318 |
. . . . . . . . 9
⊢ ((𝑁 − 𝐾) ∈ ℕ0 →
(!‘((𝑁 − 𝐾) + 1)) = ((!‘(𝑁 − 𝐾)) · ((𝑁 − 𝐾) + 1))) |
39 | 8, 38 | syl 17 |
. . . . . . . 8
⊢ (𝐾 ∈ (1...𝑁) → (!‘((𝑁 − 𝐾) + 1)) = ((!‘(𝑁 − 𝐾)) · ((𝑁 − 𝐾) + 1))) |
40 | 39 | eqcomd 2805 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → ((!‘(𝑁 − 𝐾)) · ((𝑁 − 𝐾) + 1)) = (!‘((𝑁 − 𝐾) + 1))) |
41 | | facnn2 13322 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ →
(!‘𝐾) =
((!‘(𝐾 − 1))
· 𝐾)) |
42 | 15, 41 | syl 17 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (!‘𝐾) = ((!‘(𝐾 − 1)) · 𝐾)) |
43 | 40, 42 | oveq12d 6896 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → (((!‘(𝑁 − 𝐾)) · ((𝑁 − 𝐾) + 1)) · (!‘𝐾)) = ((!‘((𝑁 − 𝐾) + 1)) · ((!‘(𝐾 − 1)) · 𝐾))) |
44 | | faccl 13323 |
. . . . . . . . 9
⊢ ((𝑁 − 𝐾) ∈ ℕ0 →
(!‘(𝑁 − 𝐾)) ∈
ℕ) |
45 | 8, 44 | syl 17 |
. . . . . . . 8
⊢ (𝐾 ∈ (1...𝑁) → (!‘(𝑁 − 𝐾)) ∈ ℕ) |
46 | 45 | nncnd 11330 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (!‘(𝑁 − 𝐾)) ∈ ℂ) |
47 | 15 | nnnn0d 11640 |
. . . . . . . . 9
⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈
ℕ0) |
48 | | faccl 13323 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ∈
ℕ) |
49 | 47, 48 | syl 17 |
. . . . . . . 8
⊢ (𝐾 ∈ (1...𝑁) → (!‘𝐾) ∈ ℕ) |
50 | 49 | nncnd 11330 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (!‘𝐾) ∈ ℂ) |
51 | 46, 50, 11 | mul32d 10536 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) · ((𝑁 − 𝐾) + 1)) = (((!‘(𝑁 − 𝐾)) · ((𝑁 − 𝐾) + 1)) · (!‘𝐾))) |
52 | 14 | nncnd 11330 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (!‘((𝑁 − 𝐾) + 1)) ∈ ℂ) |
53 | 18 | nncnd 11330 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (!‘(𝐾 − 1)) ∈
ℂ) |
54 | 52, 53, 24 | mulassd 10352 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → (((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) · 𝐾) = ((!‘((𝑁 − 𝐾) + 1)) · ((!‘(𝐾 − 1)) · 𝐾))) |
55 | 43, 51, 54 | 3eqtr4d 2843 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) · ((𝑁 − 𝐾) + 1)) = (((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) · 𝐾)) |
56 | 55 | oveq2d 6894 |
. . . 4
⊢ (𝐾 ∈ (1...𝑁) → (((!‘𝑁) · ((𝑁 − 𝐾) + 1)) / (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) · ((𝑁 − 𝐾) + 1))) = (((!‘𝑁) · ((𝑁 − 𝐾) + 1)) / (((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) · 𝐾))) |
57 | 28, 37, 56 | 3eqtr4d 2843 |
. . 3
⊢ (𝐾 ∈ (1...𝑁) → (((!‘𝑁) / ((!‘(𝑁 − (𝐾 − 1))) · (!‘(𝐾 − 1)))) · ((𝑁 − (𝐾 − 1)) / 𝐾)) = (((!‘𝑁) · ((𝑁 − 𝐾) + 1)) / (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) · ((𝑁 − 𝐾) + 1)))) |
58 | 7, 11 | mulcomd 10350 |
. . . 4
⊢ (𝐾 ∈ (1...𝑁) → ((!‘𝑁) · ((𝑁 − 𝐾) + 1)) = (((𝑁 − 𝐾) + 1) · (!‘𝑁))) |
59 | 45, 49 | nnmulcld 11366 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → ((!‘(𝑁 − 𝐾)) · (!‘𝐾)) ∈ ℕ) |
60 | 59 | nncnd 11330 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → ((!‘(𝑁 − 𝐾)) · (!‘𝐾)) ∈ ℂ) |
61 | 60, 11 | mulcomd 10350 |
. . . 4
⊢ (𝐾 ∈ (1...𝑁) → (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) · ((𝑁 − 𝐾) + 1)) = (((𝑁 − 𝐾) + 1) · ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
62 | 58, 61 | oveq12d 6896 |
. . 3
⊢ (𝐾 ∈ (1...𝑁) → (((!‘𝑁) · ((𝑁 − 𝐾) + 1)) / (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) · ((𝑁 − 𝐾) + 1))) = ((((𝑁 − 𝐾) + 1) · (!‘𝑁)) / (((𝑁 − 𝐾) + 1) · ((!‘(𝑁 − 𝐾)) · (!‘𝐾))))) |
63 | 59 | nnne0d 11363 |
. . . 4
⊢ (𝐾 ∈ (1...𝑁) → ((!‘(𝑁 − 𝐾)) · (!‘𝐾)) ≠ 0) |
64 | 10 | nnne0d 11363 |
. . . 4
⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − 𝐾) + 1) ≠ 0) |
65 | 7, 60, 11, 63, 64 | divcan5d 11119 |
. . 3
⊢ (𝐾 ∈ (1...𝑁) → ((((𝑁 − 𝐾) + 1) · (!‘𝑁)) / (((𝑁 − 𝐾) + 1) · ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
66 | 57, 62, 65 | 3eqtrrd 2838 |
. 2
⊢ (𝐾 ∈ (1...𝑁) → ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))) = (((!‘𝑁) / ((!‘(𝑁 − (𝐾 − 1))) · (!‘(𝐾 − 1)))) · ((𝑁 − (𝐾 − 1)) / 𝐾))) |
67 | | fz1ssfz0 12690 |
. . . 4
⊢
(1...𝑁) ⊆
(0...𝑁) |
68 | 67 | sseli 3794 |
. . 3
⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ (0...𝑁)) |
69 | | bcval2 13345 |
. . 3
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
70 | 68, 69 | syl 17 |
. 2
⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
71 | | ax-1cn 10282 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
72 | | npcan 10582 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
73 | 30, 71, 72 | sylancl 581 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − 1) + 1) = 𝑁) |
74 | | peano2zm 11710 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
75 | | uzid 11945 |
. . . . . . . 8
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
76 | | peano2uz 11985 |
. . . . . . . 8
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
77 | 29, 74, 75, 76 | 4syl 19 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
78 | 73, 77 | eqeltrrd 2879 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
79 | | fzss2 12635 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁)) |
80 | 78, 79 | syl 17 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → (0...(𝑁 − 1)) ⊆ (0...𝑁)) |
81 | | elfzmlbm 12704 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → (𝐾 − 1) ∈ (0...(𝑁 − 1))) |
82 | 80, 81 | sseldd 3799 |
. . . 4
⊢ (𝐾 ∈ (1...𝑁) → (𝐾 − 1) ∈ (0...𝑁)) |
83 | | bcval2 13345 |
. . . 4
⊢ ((𝐾 − 1) ∈ (0...𝑁) → (𝑁C(𝐾 − 1)) = ((!‘𝑁) / ((!‘(𝑁 − (𝐾 − 1))) · (!‘(𝐾 − 1))))) |
84 | 82, 83 | syl 17 |
. . 3
⊢ (𝐾 ∈ (1...𝑁) → (𝑁C(𝐾 − 1)) = ((!‘𝑁) / ((!‘(𝑁 − (𝐾 − 1))) · (!‘(𝐾 − 1))))) |
85 | 84 | oveq1d 6893 |
. 2
⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C(𝐾 − 1)) · ((𝑁 − (𝐾 − 1)) / 𝐾)) = (((!‘𝑁) / ((!‘(𝑁 − (𝐾 − 1))) · (!‘(𝐾 − 1)))) · ((𝑁 − (𝐾 − 1)) / 𝐾))) |
86 | 66, 70, 85 | 3eqtr4d 2843 |
1
⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · ((𝑁 − (𝐾 − 1)) / 𝐾))) |