Proof of Theorem bcm1k
Step | Hyp | Ref
| Expression |
1 | | elfzuz2 12346 |
. . . . . . . . 9
⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈
(ℤ≥‘1)) |
2 | | nnuz 11723 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
3 | 1, 2 | syl6eleqr 2712 |
. . . . . . . 8
⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ ℕ) |
4 | 3 | nnnn0d 11351 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈
ℕ0) |
5 | | faccl 13070 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → (!‘𝑁) ∈ ℕ) |
7 | 6 | nncnd 11036 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → (!‘𝑁) ∈ ℂ) |
8 | | fznn0sub 12373 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (𝑁 − 𝐾) ∈
ℕ0) |
9 | | nn0p1nn 11332 |
. . . . . . 7
⊢ ((𝑁 − 𝐾) ∈ ℕ0 → ((𝑁 − 𝐾) + 1) ∈ ℕ) |
10 | 8, 9 | syl 17 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − 𝐾) + 1) ∈ ℕ) |
11 | 10 | nncnd 11036 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − 𝐾) + 1) ∈ ℂ) |
12 | 10 | nnnn0d 11351 |
. . . . . . . 8
⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − 𝐾) + 1) ∈
ℕ0) |
13 | | faccl 13070 |
. . . . . . . 8
⊢ (((𝑁 − 𝐾) + 1) ∈ ℕ0 →
(!‘((𝑁 − 𝐾) + 1)) ∈
ℕ) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (!‘((𝑁 − 𝐾) + 1)) ∈ ℕ) |
15 | | elfznn 12370 |
. . . . . . . 8
⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ) |
16 | | nnm1nn0 11334 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈
ℕ0) |
17 | | faccl 13070 |
. . . . . . . 8
⊢ ((𝐾 − 1) ∈
ℕ0 → (!‘(𝐾 − 1)) ∈
ℕ) |
18 | 15, 16, 17 | 3syl 18 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (!‘(𝐾 − 1)) ∈
ℕ) |
19 | 14, 18 | nnmulcld 11068 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → ((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ∈
ℕ) |
20 | | nncn 11028 |
. . . . . . 7
⊢
(((!‘((𝑁
− 𝐾) + 1)) ·
(!‘(𝐾 − 1)))
∈ ℕ → ((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ∈
ℂ) |
21 | | nnne0 11053 |
. . . . . . 7
⊢
(((!‘((𝑁
− 𝐾) + 1)) ·
(!‘(𝐾 − 1)))
∈ ℕ → ((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ≠ 0) |
22 | 20, 21 | jca 554 |
. . . . . 6
⊢
(((!‘((𝑁
− 𝐾) + 1)) ·
(!‘(𝐾 − 1)))
∈ ℕ → (((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ∈ ℂ ∧
((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ≠
0)) |
23 | 19, 22 | syl 17 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → (((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ∈ ℂ ∧
((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ≠
0)) |
24 | 15 | nncnd 11036 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℂ) |
25 | 15 | nnne0d 11065 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ≠ 0) |
26 | 24, 25 | jca 554 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → (𝐾 ∈ ℂ ∧ 𝐾 ≠ 0)) |
27 | | divmuldiv 10725 |
. . . . 5
⊢
((((!‘𝑁)
∈ ℂ ∧ ((𝑁
− 𝐾) + 1) ∈
ℂ) ∧ ((((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ∈ ℂ ∧
((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) ≠ 0) ∧
(𝐾 ∈ ℂ ∧
𝐾 ≠ 0))) →
(((!‘𝑁) /
((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1)))) · (((𝑁 − 𝐾) + 1) / 𝐾)) = (((!‘𝑁) · ((𝑁 − 𝐾) + 1)) / (((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) · 𝐾))) |
28 | 7, 11, 23, 26, 27 | syl22anc 1327 |
. . . 4
⊢ (𝐾 ∈ (1...𝑁) → (((!‘𝑁) / ((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1)))) · (((𝑁 − 𝐾) + 1) / 𝐾)) = (((!‘𝑁) · ((𝑁 − 𝐾) + 1)) / (((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) · 𝐾))) |
29 | | elfzel2 12340 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ ℤ) |
30 | 29 | zcnd 11483 |
. . . . . . . . 9
⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ ℂ) |
31 | | 1cnd 10056 |
. . . . . . . . 9
⊢ (𝐾 ∈ (1...𝑁) → 1 ∈ ℂ) |
32 | 30, 24, 31 | subsubd 10420 |
. . . . . . . 8
⊢ (𝐾 ∈ (1...𝑁) → (𝑁 − (𝐾 − 1)) = ((𝑁 − 𝐾) + 1)) |
33 | 32 | fveq2d 6195 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (!‘(𝑁 − (𝐾 − 1))) = (!‘((𝑁 − 𝐾) + 1))) |
34 | 33 | oveq1d 6665 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → ((!‘(𝑁 − (𝐾 − 1))) · (!‘(𝐾 − 1))) =
((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1)))) |
35 | 34 | oveq2d 6666 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → ((!‘𝑁) / ((!‘(𝑁 − (𝐾 − 1))) · (!‘(𝐾 − 1)))) = ((!‘𝑁) / ((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))))) |
36 | 32 | oveq1d 6665 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − (𝐾 − 1)) / 𝐾) = (((𝑁 − 𝐾) + 1) / 𝐾)) |
37 | 35, 36 | oveq12d 6668 |
. . . 4
⊢ (𝐾 ∈ (1...𝑁) → (((!‘𝑁) / ((!‘(𝑁 − (𝐾 − 1))) · (!‘(𝐾 − 1)))) · ((𝑁 − (𝐾 − 1)) / 𝐾)) = (((!‘𝑁) / ((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1)))) · (((𝑁 − 𝐾) + 1) / 𝐾))) |
38 | | facp1 13065 |
. . . . . . . . 9
⊢ ((𝑁 − 𝐾) ∈ ℕ0 →
(!‘((𝑁 − 𝐾) + 1)) = ((!‘(𝑁 − 𝐾)) · ((𝑁 − 𝐾) + 1))) |
39 | 8, 38 | syl 17 |
. . . . . . . 8
⊢ (𝐾 ∈ (1...𝑁) → (!‘((𝑁 − 𝐾) + 1)) = ((!‘(𝑁 − 𝐾)) · ((𝑁 − 𝐾) + 1))) |
40 | 39 | eqcomd 2628 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → ((!‘(𝑁 − 𝐾)) · ((𝑁 − 𝐾) + 1)) = (!‘((𝑁 − 𝐾) + 1))) |
41 | | facnn2 13069 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ →
(!‘𝐾) =
((!‘(𝐾 − 1))
· 𝐾)) |
42 | 15, 41 | syl 17 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (!‘𝐾) = ((!‘(𝐾 − 1)) · 𝐾)) |
43 | 40, 42 | oveq12d 6668 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → (((!‘(𝑁 − 𝐾)) · ((𝑁 − 𝐾) + 1)) · (!‘𝐾)) = ((!‘((𝑁 − 𝐾) + 1)) · ((!‘(𝐾 − 1)) · 𝐾))) |
44 | | faccl 13070 |
. . . . . . . . 9
⊢ ((𝑁 − 𝐾) ∈ ℕ0 →
(!‘(𝑁 − 𝐾)) ∈
ℕ) |
45 | 8, 44 | syl 17 |
. . . . . . . 8
⊢ (𝐾 ∈ (1...𝑁) → (!‘(𝑁 − 𝐾)) ∈ ℕ) |
46 | 45 | nncnd 11036 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (!‘(𝑁 − 𝐾)) ∈ ℂ) |
47 | 15 | nnnn0d 11351 |
. . . . . . . . 9
⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈
ℕ0) |
48 | | faccl 13070 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ∈
ℕ) |
49 | 47, 48 | syl 17 |
. . . . . . . 8
⊢ (𝐾 ∈ (1...𝑁) → (!‘𝐾) ∈ ℕ) |
50 | 49 | nncnd 11036 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (!‘𝐾) ∈ ℂ) |
51 | 46, 50, 11 | mul32d 10246 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) · ((𝑁 − 𝐾) + 1)) = (((!‘(𝑁 − 𝐾)) · ((𝑁 − 𝐾) + 1)) · (!‘𝐾))) |
52 | 14 | nncnd 11036 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (!‘((𝑁 − 𝐾) + 1)) ∈ ℂ) |
53 | 18 | nncnd 11036 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → (!‘(𝐾 − 1)) ∈
ℂ) |
54 | 52, 53, 24 | mulassd 10063 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → (((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) · 𝐾) = ((!‘((𝑁 − 𝐾) + 1)) · ((!‘(𝐾 − 1)) · 𝐾))) |
55 | 43, 51, 54 | 3eqtr4d 2666 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) · ((𝑁 − 𝐾) + 1)) = (((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) · 𝐾)) |
56 | 55 | oveq2d 6666 |
. . . 4
⊢ (𝐾 ∈ (1...𝑁) → (((!‘𝑁) · ((𝑁 − 𝐾) + 1)) / (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) · ((𝑁 − 𝐾) + 1))) = (((!‘𝑁) · ((𝑁 − 𝐾) + 1)) / (((!‘((𝑁 − 𝐾) + 1)) · (!‘(𝐾 − 1))) · 𝐾))) |
57 | 28, 37, 56 | 3eqtr4d 2666 |
. . 3
⊢ (𝐾 ∈ (1...𝑁) → (((!‘𝑁) / ((!‘(𝑁 − (𝐾 − 1))) · (!‘(𝐾 − 1)))) · ((𝑁 − (𝐾 − 1)) / 𝐾)) = (((!‘𝑁) · ((𝑁 − 𝐾) + 1)) / (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) · ((𝑁 − 𝐾) + 1)))) |
58 | 7, 11 | mulcomd 10061 |
. . . 4
⊢ (𝐾 ∈ (1...𝑁) → ((!‘𝑁) · ((𝑁 − 𝐾) + 1)) = (((𝑁 − 𝐾) + 1) · (!‘𝑁))) |
59 | 45, 49 | nnmulcld 11068 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → ((!‘(𝑁 − 𝐾)) · (!‘𝐾)) ∈ ℕ) |
60 | 59 | nncnd 11036 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → ((!‘(𝑁 − 𝐾)) · (!‘𝐾)) ∈ ℂ) |
61 | 60, 11 | mulcomd 10061 |
. . . 4
⊢ (𝐾 ∈ (1...𝑁) → (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) · ((𝑁 − 𝐾) + 1)) = (((𝑁 − 𝐾) + 1) · ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
62 | 58, 61 | oveq12d 6668 |
. . 3
⊢ (𝐾 ∈ (1...𝑁) → (((!‘𝑁) · ((𝑁 − 𝐾) + 1)) / (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) · ((𝑁 − 𝐾) + 1))) = ((((𝑁 − 𝐾) + 1) · (!‘𝑁)) / (((𝑁 − 𝐾) + 1) · ((!‘(𝑁 − 𝐾)) · (!‘𝐾))))) |
63 | 59 | nnne0d 11065 |
. . . 4
⊢ (𝐾 ∈ (1...𝑁) → ((!‘(𝑁 − 𝐾)) · (!‘𝐾)) ≠ 0) |
64 | 10 | nnne0d 11065 |
. . . 4
⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − 𝐾) + 1) ≠ 0) |
65 | 7, 60, 11, 63, 64 | divcan5d 10827 |
. . 3
⊢ (𝐾 ∈ (1...𝑁) → ((((𝑁 − 𝐾) + 1) · (!‘𝑁)) / (((𝑁 − 𝐾) + 1) · ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
66 | 57, 62, 65 | 3eqtrrd 2661 |
. 2
⊢ (𝐾 ∈ (1...𝑁) → ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))) = (((!‘𝑁) / ((!‘(𝑁 − (𝐾 − 1))) · (!‘(𝐾 − 1)))) · ((𝑁 − (𝐾 − 1)) / 𝐾))) |
67 | | 0p1e1 11132 |
. . . . . 6
⊢ (0 + 1) =
1 |
68 | 67 | oveq1i 6660 |
. . . . 5
⊢ ((0 +
1)...𝑁) = (1...𝑁) |
69 | | 0z 11388 |
. . . . . 6
⊢ 0 ∈
ℤ |
70 | | fzp1ss 12392 |
. . . . . 6
⊢ (0 ∈
ℤ → ((0 + 1)...𝑁) ⊆ (0...𝑁)) |
71 | 69, 70 | ax-mp 5 |
. . . . 5
⊢ ((0 +
1)...𝑁) ⊆ (0...𝑁) |
72 | 68, 71 | eqsstr3i 3636 |
. . . 4
⊢
(1...𝑁) ⊆
(0...𝑁) |
73 | 72 | sseli 3599 |
. . 3
⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ (0...𝑁)) |
74 | | bcval2 13092 |
. . 3
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
75 | 73, 74 | syl 17 |
. 2
⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
76 | | ax-1cn 9994 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
77 | | npcan 10290 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
78 | 30, 76, 77 | sylancl 694 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − 1) + 1) = 𝑁) |
79 | | peano2zm 11420 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
80 | | uzid 11702 |
. . . . . . . 8
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
81 | | peano2uz 11741 |
. . . . . . . 8
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
82 | 29, 79, 80, 81 | 4syl 19 |
. . . . . . 7
⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
83 | 78, 82 | eqeltrrd 2702 |
. . . . . 6
⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) |
84 | | fzss2 12381 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁)) |
85 | 83, 84 | syl 17 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → (0...(𝑁 − 1)) ⊆ (0...𝑁)) |
86 | | elfzmlbm 12449 |
. . . . 5
⊢ (𝐾 ∈ (1...𝑁) → (𝐾 − 1) ∈ (0...(𝑁 − 1))) |
87 | 85, 86 | sseldd 3604 |
. . . 4
⊢ (𝐾 ∈ (1...𝑁) → (𝐾 − 1) ∈ (0...𝑁)) |
88 | | bcval2 13092 |
. . . 4
⊢ ((𝐾 − 1) ∈ (0...𝑁) → (𝑁C(𝐾 − 1)) = ((!‘𝑁) / ((!‘(𝑁 − (𝐾 − 1))) · (!‘(𝐾 − 1))))) |
89 | 87, 88 | syl 17 |
. . 3
⊢ (𝐾 ∈ (1...𝑁) → (𝑁C(𝐾 − 1)) = ((!‘𝑁) / ((!‘(𝑁 − (𝐾 − 1))) · (!‘(𝐾 − 1))))) |
90 | 89 | oveq1d 6665 |
. 2
⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C(𝐾 − 1)) · ((𝑁 − (𝐾 − 1)) / 𝐾)) = (((!‘𝑁) / ((!‘(𝑁 − (𝐾 − 1))) · (!‘(𝐾 − 1)))) · ((𝑁 − (𝐾 − 1)) / 𝐾))) |
91 | 66, 75, 90 | 3eqtr4d 2666 |
1
⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · ((𝑁 − (𝐾 − 1)) / 𝐾))) |