Proof of Theorem bccmpl
| Step | Hyp | Ref
| Expression |
| 1 | | bcval2 14344 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
| 2 | | fznn0sub2 13675 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 − 𝐾) ∈ (0...𝑁)) |
| 3 | | bcval2 14344 |
. . . . . 6
⊢ ((𝑁 − 𝐾) ∈ (0...𝑁) → (𝑁C(𝑁 − 𝐾)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑁 − 𝐾))) · (!‘(𝑁 − 𝐾))))) |
| 4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C(𝑁 − 𝐾)) = ((!‘𝑁) / ((!‘(𝑁 − (𝑁 − 𝐾))) · (!‘(𝑁 − 𝐾))))) |
| 5 | | elfznn0 13660 |
. . . . . . . . . . 11
⊢ ((𝑁 − 𝐾) ∈ (0...𝑁) → (𝑁 − 𝐾) ∈
ℕ0) |
| 6 | 5 | faccld 14323 |
. . . . . . . . . 10
⊢ ((𝑁 − 𝐾) ∈ (0...𝑁) → (!‘(𝑁 − 𝐾)) ∈ ℕ) |
| 7 | 6 | nncnd 12282 |
. . . . . . . . 9
⊢ ((𝑁 − 𝐾) ∈ (0...𝑁) → (!‘(𝑁 − 𝐾)) ∈ ℂ) |
| 8 | 2, 7 | syl 17 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → (!‘(𝑁 − 𝐾)) ∈ ℂ) |
| 9 | | elfznn0 13660 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈
ℕ0) |
| 10 | 9 | faccld 14323 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0...𝑁) → (!‘𝐾) ∈ ℕ) |
| 11 | 10 | nncnd 12282 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → (!‘𝐾) ∈ ℂ) |
| 12 | 8, 11 | mulcomd 11282 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → ((!‘(𝑁 − 𝐾)) · (!‘𝐾)) = ((!‘𝐾) · (!‘(𝑁 − 𝐾)))) |
| 13 | | elfz3nn0 13661 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (0...𝑁) → 𝑁 ∈
ℕ0) |
| 14 | | elfzelz 13564 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℤ) |
| 15 | | nn0cn 12536 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
| 16 | | zcn 12618 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℂ) |
| 17 | | nncan 11538 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℂ ∧ 𝐾 ∈ ℂ) → (𝑁 − (𝑁 − 𝐾)) = 𝐾) |
| 18 | 15, 16, 17 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ (𝑁 − (𝑁 − 𝐾)) = 𝐾) |
| 19 | 13, 14, 18 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 − (𝑁 − 𝐾)) = 𝐾) |
| 20 | 19 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → (!‘(𝑁 − (𝑁 − 𝐾))) = (!‘𝐾)) |
| 21 | 20 | oveq1d 7446 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → ((!‘(𝑁 − (𝑁 − 𝐾))) · (!‘(𝑁 − 𝐾))) = ((!‘𝐾) · (!‘(𝑁 − 𝐾)))) |
| 22 | 12, 21 | eqtr4d 2780 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → ((!‘(𝑁 − 𝐾)) · (!‘𝐾)) = ((!‘(𝑁 − (𝑁 − 𝐾))) · (!‘(𝑁 − 𝐾)))) |
| 23 | 22 | oveq2d 7447 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))) = ((!‘𝑁) / ((!‘(𝑁 − (𝑁 − 𝐾))) · (!‘(𝑁 − 𝐾))))) |
| 24 | 4, 23 | eqtr4d 2780 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C(𝑁 − 𝐾)) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
| 25 | 1, 24 | eqtr4d 2780 |
. . 3
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = (𝑁C(𝑁 − 𝐾))) |
| 26 | 25 | adantl 481 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = (𝑁C(𝑁 − 𝐾))) |
| 27 | | bcval3 14345 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = 0) |
| 28 | | simp1 1137 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ
∧ ¬ 𝐾 ∈
(0...𝑁)) → 𝑁 ∈
ℕ0) |
| 29 | | nn0z 12638 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
| 30 | | zsubcl 12659 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 − 𝐾) ∈ ℤ) |
| 31 | 29, 30 | sylan 580 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ (𝑁 − 𝐾) ∈
ℤ) |
| 32 | 31 | 3adant3 1133 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁 − 𝐾) ∈ ℤ) |
| 33 | | fznn0sub2 13675 |
. . . . . . . 8
⊢ ((𝑁 − 𝐾) ∈ (0...𝑁) → (𝑁 − (𝑁 − 𝐾)) ∈ (0...𝑁)) |
| 34 | 18 | eleq1d 2826 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ ((𝑁 − (𝑁 − 𝐾)) ∈ (0...𝑁) ↔ 𝐾 ∈ (0...𝑁))) |
| 35 | 33, 34 | imbitrid 244 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ ((𝑁 − 𝐾) ∈ (0...𝑁) → 𝐾 ∈ (0...𝑁))) |
| 36 | 35 | con3d 152 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ (¬ 𝐾 ∈
(0...𝑁) → ¬ (𝑁 − 𝐾) ∈ (0...𝑁))) |
| 37 | 36 | 3impia 1118 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ
∧ ¬ 𝐾 ∈
(0...𝑁)) → ¬
(𝑁 − 𝐾) ∈ (0...𝑁)) |
| 38 | | bcval3 14345 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑁 − 𝐾) ∈ ℤ ∧ ¬
(𝑁 − 𝐾) ∈ (0...𝑁)) → (𝑁C(𝑁 − 𝐾)) = 0) |
| 39 | 28, 32, 37, 38 | syl3anc 1373 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C(𝑁 − 𝐾)) = 0) |
| 40 | 27, 39 | eqtr4d 2780 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = (𝑁C(𝑁 − 𝐾))) |
| 41 | 40 | 3expa 1119 |
. 2
⊢ (((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
∧ ¬ 𝐾 ∈
(0...𝑁)) → (𝑁C𝐾) = (𝑁C(𝑁 − 𝐾))) |
| 42 | 26, 41 | pm2.61dan 813 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐾 ∈ ℤ)
→ (𝑁C𝐾) = (𝑁C(𝑁 − 𝐾))) |