Proof of Theorem bcp1nk
| Step | Hyp | Ref
| Expression |
| 1 | | elfzel1 13563 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → 0 ∈ ℤ) |
| 2 | | elfzel2 13562 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → 𝑁 ∈ ℤ) |
| 3 | | elfzelz 13564 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℤ) |
| 4 | | 1zzd 12648 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → 1 ∈ ℤ) |
| 5 | | fzaddel 13598 |
. . . . . 6
⊢ (((0
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ (𝐾
∈ ℤ ∧ 1 ∈ ℤ)) → (𝐾 ∈ (0...𝑁) ↔ (𝐾 + 1) ∈ ((0 + 1)...(𝑁 + 1)))) |
| 6 | 1, 2, 3, 4, 5 | syl22anc 839 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → (𝐾 ∈ (0...𝑁) ↔ (𝐾 + 1) ∈ ((0 + 1)...(𝑁 + 1)))) |
| 7 | 6 | ibi 267 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → (𝐾 + 1) ∈ ((0 + 1)...(𝑁 + 1))) |
| 8 | | 1e0p1 12775 |
. . . . 5
⊢ 1 = (0 +
1) |
| 9 | 8 | oveq1i 7441 |
. . . 4
⊢
(1...(𝑁 + 1)) = ((0
+ 1)...(𝑁 +
1)) |
| 10 | 7, 9 | eleqtrrdi 2852 |
. . 3
⊢ (𝐾 ∈ (0...𝑁) → (𝐾 + 1) ∈ (1...(𝑁 + 1))) |
| 11 | | bcm1k 14354 |
. . 3
⊢ ((𝐾 + 1) ∈ (1...(𝑁 + 1)) → ((𝑁 + 1)C(𝐾 + 1)) = (((𝑁 + 1)C((𝐾 + 1) − 1)) · (((𝑁 + 1) − ((𝐾 + 1) − 1)) / (𝐾 + 1)))) |
| 12 | 10, 11 | syl 17 |
. 2
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1)C(𝐾 + 1)) = (((𝑁 + 1)C((𝐾 + 1) − 1)) · (((𝑁 + 1) − ((𝐾 + 1) − 1)) / (𝐾 + 1)))) |
| 13 | 3 | zcnd 12723 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℂ) |
| 14 | | ax-1cn 11213 |
. . . . . . 7
⊢ 1 ∈
ℂ |
| 15 | | pncan 11514 |
. . . . . . 7
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐾 + 1)
− 1) = 𝐾) |
| 16 | 13, 14, 15 | sylancl 586 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → ((𝐾 + 1) − 1) = 𝐾) |
| 17 | 16 | oveq2d 7447 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1)C((𝐾 + 1) − 1)) = ((𝑁 + 1)C𝐾)) |
| 18 | | bcp1n 14355 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1)C𝐾) = ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾)))) |
| 19 | 17, 18 | eqtrd 2777 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1)C((𝐾 + 1) − 1)) = ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾)))) |
| 20 | 16 | oveq2d 7447 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1) − ((𝐾 + 1) − 1)) = ((𝑁 + 1) − 𝐾)) |
| 21 | 20 | oveq1d 7446 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → (((𝑁 + 1) − ((𝐾 + 1) − 1)) / (𝐾 + 1)) = (((𝑁 + 1) − 𝐾) / (𝐾 + 1))) |
| 22 | 19, 21 | oveq12d 7449 |
. . 3
⊢ (𝐾 ∈ (0...𝑁) → (((𝑁 + 1)C((𝐾 + 1) − 1)) · (((𝑁 + 1) − ((𝐾 + 1) − 1)) / (𝐾 + 1))) = (((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) · (((𝑁 + 1) − 𝐾) / (𝐾 + 1)))) |
| 23 | | bcrpcl 14347 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) ∈
ℝ+) |
| 24 | 23 | rpcnd 13079 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) ∈ ℂ) |
| 25 | 2 | peano2zd 12725 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 + 1) ∈ ℤ) |
| 26 | 25 | zred 12722 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 + 1) ∈ ℝ) |
| 27 | 3 | zred 12722 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℝ) |
| 28 | 2 | zred 12722 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0...𝑁) → 𝑁 ∈ ℝ) |
| 29 | | elfzle2 13568 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ≤ 𝑁) |
| 30 | 28 | ltp1d 12198 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0...𝑁) → 𝑁 < (𝑁 + 1)) |
| 31 | 27, 28, 26, 29, 30 | lelttrd 11419 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 < (𝑁 + 1)) |
| 32 | | znnsub 12663 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ) →
(𝐾 < (𝑁 + 1) ↔ ((𝑁 + 1) − 𝐾) ∈ ℕ)) |
| 33 | 3, 25, 32 | syl2anc 584 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → (𝐾 < (𝑁 + 1) ↔ ((𝑁 + 1) − 𝐾) ∈ ℕ)) |
| 34 | 31, 33 | mpbid 232 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℕ) |
| 35 | 26, 34 | nndivred 12320 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1) / ((𝑁 + 1) − 𝐾)) ∈ ℝ) |
| 36 | 35 | recnd 11289 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1) / ((𝑁 + 1) − 𝐾)) ∈ ℂ) |
| 37 | 34 | nnred 12281 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℝ) |
| 38 | | elfznn0 13660 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈
ℕ0) |
| 39 | | nn0p1nn 12565 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ (𝐾 + 1) ∈
ℕ) |
| 40 | 38, 39 | syl 17 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → (𝐾 + 1) ∈ ℕ) |
| 41 | 37, 40 | nndivred 12320 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → (((𝑁 + 1) − 𝐾) / (𝐾 + 1)) ∈ ℝ) |
| 42 | 41 | recnd 11289 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → (((𝑁 + 1) − 𝐾) / (𝐾 + 1)) ∈ ℂ) |
| 43 | 24, 36, 42 | mulassd 11284 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → (((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) · (((𝑁 + 1) − 𝐾) / (𝐾 + 1))) = ((𝑁C𝐾) · (((𝑁 + 1) / ((𝑁 + 1) − 𝐾)) · (((𝑁 + 1) − 𝐾) / (𝐾 + 1))))) |
| 44 | 25 | zcnd 12723 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 + 1) ∈ ℂ) |
| 45 | 34 | nncnd 12282 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℂ) |
| 46 | 40 | nncnd 12282 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → (𝐾 + 1) ∈ ℂ) |
| 47 | 34 | nnne0d 12316 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1) − 𝐾) ≠ 0) |
| 48 | 40 | nnne0d 12316 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → (𝐾 + 1) ≠ 0) |
| 49 | 44, 45, 46, 47, 48 | dmdcan2d 12073 |
. . . . 5
⊢ (𝐾 ∈ (0...𝑁) → (((𝑁 + 1) / ((𝑁 + 1) − 𝐾)) · (((𝑁 + 1) − 𝐾) / (𝐾 + 1))) = ((𝑁 + 1) / (𝐾 + 1))) |
| 50 | 49 | oveq2d 7447 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁C𝐾) · (((𝑁 + 1) / ((𝑁 + 1) − 𝐾)) · (((𝑁 + 1) − 𝐾) / (𝐾 + 1)))) = ((𝑁C𝐾) · ((𝑁 + 1) / (𝐾 + 1)))) |
| 51 | 43, 50 | eqtrd 2777 |
. . 3
⊢ (𝐾 ∈ (0...𝑁) → (((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) · (((𝑁 + 1) − 𝐾) / (𝐾 + 1))) = ((𝑁C𝐾) · ((𝑁 + 1) / (𝐾 + 1)))) |
| 52 | 22, 51 | eqtrd 2777 |
. 2
⊢ (𝐾 ∈ (0...𝑁) → (((𝑁 + 1)C((𝐾 + 1) − 1)) · (((𝑁 + 1) − ((𝐾 + 1) − 1)) / (𝐾 + 1))) = ((𝑁C𝐾) · ((𝑁 + 1) / (𝐾 + 1)))) |
| 53 | 12, 52 | eqtrd 2777 |
1
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1)C(𝐾 + 1)) = ((𝑁C𝐾) · ((𝑁 + 1) / (𝐾 + 1)))) |