Proof of Theorem binom1dif
| Step | Hyp | Ref
| Expression |
| 1 | | fzfid 14014 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (0...(𝑁 − 1))
∈ Fin) |
| 2 | | fzssp1 13607 |
. . . . . 6
⊢
(0...(𝑁 − 1))
⊆ (0...((𝑁 − 1)
+ 1)) |
| 3 | | nn0cn 12536 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
| 4 | 3 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℂ) |
| 5 | | ax-1cn 11213 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
| 6 | | npcan 11517 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
| 7 | 4, 5, 6 | sylancl 586 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝑁 − 1) + 1)
= 𝑁) |
| 8 | 7 | oveq2d 7447 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (0...((𝑁 − 1)
+ 1)) = (0...𝑁)) |
| 9 | 2, 8 | sseqtrid 4026 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (0...(𝑁 − 1))
⊆ (0...𝑁)) |
| 10 | 9 | sselda 3983 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ (0...𝑁)) |
| 11 | | bccl2 14362 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑁) → (𝑁C𝑘) ∈ ℕ) |
| 12 | 11 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈ ℕ) |
| 13 | 12 | nncnd 12282 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈ ℂ) |
| 14 | | simpl 482 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℂ) |
| 15 | | elfznn0 13660 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
| 16 | | expcl 14120 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℂ) |
| 17 | 14, 15, 16 | syl2an 596 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (𝐴↑𝑘) ∈ ℂ) |
| 18 | 13, 17 | mulcld 11281 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (𝐴↑𝑘)) ∈ ℂ) |
| 19 | 10, 18 | syldan 591 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁C𝑘) · (𝐴↑𝑘)) ∈ ℂ) |
| 20 | 1, 19 | fsumcl 15769 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ Σ𝑘 ∈
(0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) ∈ ℂ) |
| 21 | | expcl 14120 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝐴↑𝑁) ∈
ℂ) |
| 22 | | addcom 11447 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 + 1) =
(1 + 𝐴)) |
| 23 | 14, 5, 22 | sylancl 586 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 + 1) = (1 + 𝐴)) |
| 24 | 23 | oveq1d 7446 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 + 1)↑𝑁) = ((1 + 𝐴)↑𝑁)) |
| 25 | | binom1p 15867 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((1 + 𝐴)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · (𝐴↑𝑘))) |
| 26 | | simpr 484 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℕ0) |
| 27 | | nn0uz 12920 |
. . . . . 6
⊢
ℕ0 = (ℤ≥‘0) |
| 28 | 26, 27 | eleqtrdi 2851 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
(ℤ≥‘0)) |
| 29 | | oveq2 7439 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (𝑁C𝑘) = (𝑁C𝑁)) |
| 30 | | oveq2 7439 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (𝐴↑𝑘) = (𝐴↑𝑁)) |
| 31 | 29, 30 | oveq12d 7449 |
. . . . 5
⊢ (𝑘 = 𝑁 → ((𝑁C𝑘) · (𝐴↑𝑘)) = ((𝑁C𝑁) · (𝐴↑𝑁))) |
| 32 | 28, 18, 31 | fsumm1 15787 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ Σ𝑘 ∈
(0...𝑁)((𝑁C𝑘) · (𝐴↑𝑘)) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) + ((𝑁C𝑁) · (𝐴↑𝑁)))) |
| 33 | | bcnn 14351 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑁C𝑁) = 1) |
| 34 | 33 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝑁C𝑁) = 1) |
| 35 | 34 | oveq1d 7446 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝑁C𝑁) · (𝐴↑𝑁)) = (1 · (𝐴↑𝑁))) |
| 36 | 21 | mullidd 11279 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (1 · (𝐴↑𝑁)) = (𝐴↑𝑁)) |
| 37 | 35, 36 | eqtrd 2777 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝑁C𝑁) · (𝐴↑𝑁)) = (𝐴↑𝑁)) |
| 38 | 37 | oveq2d 7447 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (Σ𝑘 ∈
(0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) + ((𝑁C𝑁) · (𝐴↑𝑁))) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) + (𝐴↑𝑁))) |
| 39 | 32, 38 | eqtrd 2777 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ Σ𝑘 ∈
(0...𝑁)((𝑁C𝑘) · (𝐴↑𝑘)) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) + (𝐴↑𝑁))) |
| 40 | 24, 25, 39 | 3eqtrd 2781 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 + 1)↑𝑁) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) + (𝐴↑𝑁))) |
| 41 | 20, 21, 40 | mvrraddd 11675 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (((𝐴 + 1)↑𝑁) − (𝐴↑𝑁)) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘))) |