Proof of Theorem bcp1n
Step | Hyp | Ref
| Expression |
1 | | elfz3nn0 12303 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → 𝑁 ∈
ℕ0) |
2 | | facp1 12927 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (!‘(𝑁 + 1)) =
((!‘𝑁) ·
(𝑁 + 1))) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1))) |
4 | | fznn0sub 12244 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 − 𝐾) ∈
ℕ0) |
5 | | facp1 12927 |
. . . . . . . 8
⊢ ((𝑁 − 𝐾) ∈ ℕ0 →
(!‘((𝑁 − 𝐾) + 1)) = ((!‘(𝑁 − 𝐾)) · ((𝑁 − 𝐾) + 1))) |
6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → (!‘((𝑁 − 𝐾) + 1)) = ((!‘(𝑁 − 𝐾)) · ((𝑁 − 𝐾) + 1))) |
7 | 1 | nn0cnd 11230 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0...𝑁) → 𝑁 ∈ ℂ) |
8 | | 1cnd 9935 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0...𝑁) → 1 ∈ ℂ) |
9 | | elfznn0 12302 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈
ℕ0) |
10 | 9 | nn0cnd 11230 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℂ) |
11 | 7, 8, 10 | addsubd 10292 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1) − 𝐾) = ((𝑁 − 𝐾) + 1)) |
12 | 11 | fveq2d 6107 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → (!‘((𝑁 + 1) − 𝐾)) = (!‘((𝑁 − 𝐾) + 1))) |
13 | 11 | oveq2d 6565 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → ((!‘(𝑁 − 𝐾)) · ((𝑁 + 1) − 𝐾)) = ((!‘(𝑁 − 𝐾)) · ((𝑁 − 𝐾) + 1))) |
14 | 6, 12, 13 | 3eqtr4d 2654 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → (!‘((𝑁 + 1) − 𝐾)) = ((!‘(𝑁 − 𝐾)) · ((𝑁 + 1) − 𝐾))) |
15 | 14 | oveq1d 6564 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → ((!‘((𝑁 + 1) − 𝐾)) · (!‘𝐾)) = (((!‘(𝑁 − 𝐾)) · ((𝑁 + 1) − 𝐾)) · (!‘𝐾))) |
16 | | faccl 12932 |
. . . . . . . 8
⊢ ((𝑁 − 𝐾) ∈ ℕ0 →
(!‘(𝑁 − 𝐾)) ∈
ℕ) |
17 | 4, 16 | syl 17 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → (!‘(𝑁 − 𝐾)) ∈ ℕ) |
18 | 17 | nncnd 10913 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → (!‘(𝑁 − 𝐾)) ∈ ℂ) |
19 | | nn0p1nn 11209 |
. . . . . . . . 9
⊢ ((𝑁 − 𝐾) ∈ ℕ0 → ((𝑁 − 𝐾) + 1) ∈ ℕ) |
20 | 4, 19 | syl 17 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 − 𝐾) + 1) ∈ ℕ) |
21 | 11, 20 | eqeltrd 2688 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℕ) |
22 | 21 | nncnd 10913 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℂ) |
23 | | faccl 12932 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ∈
ℕ) |
24 | 9, 23 | syl 17 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → (!‘𝐾) ∈ ℕ) |
25 | 24 | nncnd 10913 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → (!‘𝐾) ∈ ℂ) |
26 | 18, 22, 25 | mul32d 10125 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → (((!‘(𝑁 − 𝐾)) · ((𝑁 + 1) − 𝐾)) · (!‘𝐾)) = (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) · ((𝑁 + 1) − 𝐾))) |
27 | 15, 26 | eqtrd 2644 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → ((!‘((𝑁 + 1) − 𝐾)) · (!‘𝐾)) = (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) · ((𝑁 + 1) − 𝐾))) |
28 | 3, 27 | oveq12d 6567 |
. . 3
⊢ (𝐾 ∈ (0...𝑁) → ((!‘(𝑁 + 1)) / ((!‘((𝑁 + 1) − 𝐾)) · (!‘𝐾))) = (((!‘𝑁) · (𝑁 + 1)) / (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) · ((𝑁 + 1) − 𝐾)))) |
29 | | faccl 12932 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
30 | 1, 29 | syl 17 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → (!‘𝑁) ∈ ℕ) |
31 | 30 | nncnd 10913 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → (!‘𝑁) ∈ ℂ) |
32 | | nn0p1nn 11209 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
33 | 1, 32 | syl 17 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 + 1) ∈ ℕ) |
34 | 33 | nncnd 10913 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 + 1) ∈ ℂ) |
35 | 17, 24 | nnmulcld 10945 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → ((!‘(𝑁 − 𝐾)) · (!‘𝐾)) ∈ ℕ) |
36 | | nncn 10905 |
. . . . . 6
⊢
(((!‘(𝑁
− 𝐾)) ·
(!‘𝐾)) ∈ ℕ
→ ((!‘(𝑁 −
𝐾)) · (!‘𝐾)) ∈
ℂ) |
37 | | nnne0 10930 |
. . . . . 6
⊢
(((!‘(𝑁
− 𝐾)) ·
(!‘𝐾)) ∈ ℕ
→ ((!‘(𝑁 −
𝐾)) · (!‘𝐾)) ≠ 0) |
38 | 36, 37 | jca 553 |
. . . . 5
⊢
(((!‘(𝑁
− 𝐾)) ·
(!‘𝐾)) ∈ ℕ
→ (((!‘(𝑁
− 𝐾)) ·
(!‘𝐾)) ∈ ℂ
∧ ((!‘(𝑁 −
𝐾)) · (!‘𝐾)) ≠ 0)) |
39 | 35, 38 | syl 17 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) ∈ ℂ ∧ ((!‘(𝑁 − 𝐾)) · (!‘𝐾)) ≠ 0)) |
40 | 21 | nnne0d 10942 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1) − 𝐾) ≠ 0) |
41 | 22, 40 | jca 553 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → (((𝑁 + 1) − 𝐾) ∈ ℂ ∧ ((𝑁 + 1) − 𝐾) ≠ 0)) |
42 | | divmuldiv 10604 |
. . . 4
⊢
((((!‘𝑁)
∈ ℂ ∧ (𝑁 +
1) ∈ ℂ) ∧ ((((!‘(𝑁 − 𝐾)) · (!‘𝐾)) ∈ ℂ ∧ ((!‘(𝑁 − 𝐾)) · (!‘𝐾)) ≠ 0) ∧ (((𝑁 + 1) − 𝐾) ∈ ℂ ∧ ((𝑁 + 1) − 𝐾) ≠ 0))) → (((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = (((!‘𝑁) · (𝑁 + 1)) / (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) · ((𝑁 + 1) − 𝐾)))) |
43 | 31, 34, 39, 41, 42 | syl22anc 1319 |
. . 3
⊢ (𝐾 ∈ (0...𝑁) → (((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = (((!‘𝑁) · (𝑁 + 1)) / (((!‘(𝑁 − 𝐾)) · (!‘𝐾)) · ((𝑁 + 1) − 𝐾)))) |
44 | 28, 43 | eqtr4d 2647 |
. 2
⊢ (𝐾 ∈ (0...𝑁) → ((!‘(𝑁 + 1)) / ((!‘((𝑁 + 1) − 𝐾)) · (!‘𝐾))) = (((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾)))) |
45 | | fzelp1 12263 |
. . 3
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ (0...(𝑁 + 1))) |
46 | | bcval2 12954 |
. . 3
⊢ (𝐾 ∈ (0...(𝑁 + 1)) → ((𝑁 + 1)C𝐾) = ((!‘(𝑁 + 1)) / ((!‘((𝑁 + 1) − 𝐾)) · (!‘𝐾)))) |
47 | 45, 46 | syl 17 |
. 2
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1)C𝐾) = ((!‘(𝑁 + 1)) / ((!‘((𝑁 + 1) − 𝐾)) · (!‘𝐾)))) |
48 | | bcval2 12954 |
. . 3
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) |
49 | 48 | oveq1d 6564 |
. 2
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = (((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾)))) |
50 | 44, 47, 49 | 3eqtr4d 2654 |
1
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1)C𝐾) = ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾)))) |