Proof of Theorem bccmpl
Step | Hyp | Ref
| Expression |
1 | | bcval2 13345 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
2 | | fznn0sub2 12701 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 − 𝐾) ∈ (0...𝑁)) |
3 | | bcval2 13345 |
. . . . . 6
⊢ ((𝑁 − 𝐾) ∈ (0...𝑁) → (𝑁C(𝑁 − 𝐾)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑁 − 𝐾))) · (!‘(𝑁 − 𝐾))))) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C(𝑁 − 𝐾)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑁 − 𝐾))) · (!‘(𝑁 − 𝐾))))) |
5 | | elfznn0 12687 |
. . . . . . . . . . 11
⊢ ((𝑁 − 𝐾) ∈ (0...𝑁) → (𝑁 − 𝐾) ∈
ℕ0) |
6 | | faccl 13323 |
. . . . . . . . . . 11
⊢ ((𝑁 − 𝐾) ∈ ℕ0 →
(!‘(𝑁 − 𝐾)) ∈
ℕ) |
7 | 5, 6 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 − 𝐾) ∈ (0...𝑁) → (!‘(𝑁 − 𝐾)) ∈ ℕ) |
8 | 7 | nncnd 11330 |
. . . . . . . . 9
⊢ ((𝑁 − 𝐾) ∈ (0...𝑁) → (!‘(𝑁 − 𝐾)) ∈ ℂ) |
9 | 2, 8 | syl 17 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → (!‘(𝑁 − 𝐾)) ∈ ℂ) |
10 | | elfznn0 12687 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈
ℕ0) |
11 | | faccl 13323 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ∈
ℕ) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0...𝑁) → (!‘𝐾) ∈ ℕ) |
13 | 12 | nncnd 11330 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → (!‘𝐾) ∈ ℂ) |
14 | 9, 13 | mulcomd 10350 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → ((!‘(𝑁 − 𝐾)) · (!‘𝐾)) = ((!‘𝐾) · (!‘(𝑁 − 𝐾)))) |
15 | | elfz3nn0 12688 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (0...𝑁) → 𝑁 ∈
ℕ0) |
16 | | elfzelz 12596 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℤ) |
17 | | nn0cn 11591 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
18 | | zcn 11671 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℂ) |
19 | | nncan 10602 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℂ ∧ 𝐾 ∈ ℂ) → (𝑁 − (𝑁 − 𝐾)) = 𝐾) |
20 | 17, 18, 19 | syl2an 590 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ (𝑁 − (𝑁 − 𝐾)) = 𝐾) |
21 | 15, 16, 20 | syl2anc 580 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 − (𝑁 − 𝐾)) = 𝐾) |
22 | 21 | fveq2d 6415 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → (!‘(𝑁 − (𝑁 − 𝐾))) = (!‘𝐾)) |
23 | 22 | oveq1d 6893 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → ((!‘(𝑁 − (𝑁 − 𝐾))) · (!‘(𝑁 − 𝐾))) = ((!‘𝐾) · (!‘(𝑁 − 𝐾)))) |
24 | 14, 23 | eqtr4d 2836 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → ((!‘(𝑁 − 𝐾)) · (!‘𝐾)) = ((!‘(𝑁 − (𝑁 − 𝐾))) · (!‘(𝑁 − 𝐾)))) |
25 | 24 | oveq2d 6894 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))) = ((!‘𝑁) / ((!‘(𝑁 − (𝑁 − 𝐾))) · (!‘(𝑁 − 𝐾))))) |
26 | 4, 25 | eqtr4d 2836 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C(𝑁 − 𝐾)) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
27 | 1, 26 | eqtr4d 2836 |
. . 3
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = (𝑁C(𝑁 − 𝐾))) |
28 | 27 | adantl 474 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = (𝑁C(𝑁 − 𝐾))) |
29 | | bcval3 13346 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = 0) |
30 | | simp1 1167 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝑁 ∈
ℕ0) |
31 | | nn0z 11690 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
32 | | zsubcl 11709 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 − 𝐾) ∈ ℤ) |
33 | 31, 32 | sylan 576 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ (𝑁 − 𝐾) ∈
ℤ) |
34 | 33 | 3adant3 1163 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁 − 𝐾) ∈ ℤ) |
35 | | fznn0sub2 12701 |
. . . . . . . 8
⊢ ((𝑁 − 𝐾) ∈ (0...𝑁) → (𝑁 − (𝑁 − 𝐾)) ∈ (0...𝑁)) |
36 | 20 | eleq1d 2863 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ ((𝑁 − (𝑁 − 𝐾)) ∈ (0...𝑁) ↔ 𝐾 ∈ (0...𝑁))) |
37 | 35, 36 | syl5ib 236 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ ((𝑁 − 𝐾) ∈ (0...𝑁) → 𝐾 ∈ (0...𝑁))) |
38 | 37 | con3d 150 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ (¬ 𝐾 ∈
(0...𝑁) → ¬ (𝑁 − 𝐾) ∈ (0...𝑁))) |
39 | 38 | 3impia 1146 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ
∧ ¬ 𝐾 ∈
(0...𝑁)) → ¬
(𝑁 − 𝐾) ∈ (0...𝑁)) |
40 | | bcval3 13346 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑁 − 𝐾) ∈ ℤ ∧ ¬
(𝑁 − 𝐾) ∈ (0...𝑁)) → (𝑁C(𝑁 − 𝐾)) = 0) |
41 | 30, 34, 39, 40 | syl3anc 1491 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C(𝑁 − 𝐾)) = 0) |
42 | 29, 41 | eqtr4d 2836 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = (𝑁C(𝑁 − 𝐾))) |
43 | 42 | 3expa 1148 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = (𝑁C(𝑁 − 𝐾))) |
44 | 28, 43 | pm2.61dan 848 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ (𝑁C𝐾) = (𝑁C(𝑁 − 𝐾))) |