Proof of Theorem binom1dif
Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℂ) |
2 | | ax-1cn 9994 |
. . . . . 6
⊢ 1 ∈
ℂ |
3 | | addcom 10222 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 + 1) =
(1 + 𝐴)) |
4 | 1, 2, 3 | sylancl 694 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 + 1) = (1 + 𝐴)) |
5 | 4 | oveq1d 6665 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 + 1)↑𝑁) = ((1 + 𝐴)↑𝑁)) |
6 | | binom1p 14563 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((1 + 𝐴)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · (𝐴↑𝑘))) |
7 | | simpr 477 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℕ0) |
8 | | nn0uz 11722 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
9 | 7, 8 | syl6eleq 2711 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
(ℤ≥‘0)) |
10 | | bccl2 13110 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → (𝑁C𝑘) ∈ ℕ) |
11 | 10 | adantl 482 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈ ℕ) |
12 | 11 | nncnd 11036 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈ ℂ) |
13 | | elfznn0 12433 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
14 | | expcl 12878 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℂ) |
15 | 1, 13, 14 | syl2an 494 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (𝐴↑𝑘) ∈ ℂ) |
16 | 12, 15 | mulcld 10060 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (𝐴↑𝑘)) ∈ ℂ) |
17 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → (𝑁C𝑘) = (𝑁C𝑁)) |
18 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → (𝐴↑𝑘) = (𝐴↑𝑁)) |
19 | 17, 18 | oveq12d 6668 |
. . . . . 6
⊢ (𝑘 = 𝑁 → ((𝑁C𝑘) · (𝐴↑𝑘)) = ((𝑁C𝑁) · (𝐴↑𝑁))) |
20 | 9, 16, 19 | fsumm1 14480 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ Σ𝑘 ∈
(0...𝑁)((𝑁C𝑘) · (𝐴↑𝑘)) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) + ((𝑁C𝑁) · (𝐴↑𝑁)))) |
21 | | bcnn 13099 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑁C𝑁) = 1) |
22 | 21 | adantl 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝑁C𝑁) = 1) |
23 | 22 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝑁C𝑁) · (𝐴↑𝑁)) = (1 · (𝐴↑𝑁))) |
24 | | expcl 12878 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝐴↑𝑁) ∈
ℂ) |
25 | 24 | mulid2d 10058 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (1 · (𝐴↑𝑁)) = (𝐴↑𝑁)) |
26 | 23, 25 | eqtrd 2656 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝑁C𝑁) · (𝐴↑𝑁)) = (𝐴↑𝑁)) |
27 | 26 | oveq2d 6666 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (Σ𝑘 ∈
(0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) + ((𝑁C𝑁) · (𝐴↑𝑁))) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) + (𝐴↑𝑁))) |
28 | 20, 27 | eqtrd 2656 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ Σ𝑘 ∈
(0...𝑁)((𝑁C𝑘) · (𝐴↑𝑘)) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) + (𝐴↑𝑁))) |
29 | 5, 6, 28 | 3eqtrd 2660 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 + 1)↑𝑁) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) + (𝐴↑𝑁))) |
30 | 29 | oveq1d 6665 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (((𝐴 + 1)↑𝑁) − (𝐴↑𝑁)) = ((Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) + (𝐴↑𝑁)) − (𝐴↑𝑁))) |
31 | | fzfid 12772 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (0...(𝑁 − 1))
∈ Fin) |
32 | | fzssp1 12384 |
. . . . . . 7
⊢
(0...(𝑁 − 1))
⊆ (0...((𝑁 − 1)
+ 1)) |
33 | | nn0cn 11302 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
34 | 33 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℂ) |
35 | | npcan 10290 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
36 | 34, 2, 35 | sylancl 694 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝑁 − 1) + 1)
= 𝑁) |
37 | 36 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (0...((𝑁 − 1)
+ 1)) = (0...𝑁)) |
38 | 32, 37 | syl5sseq 3653 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (0...(𝑁 − 1))
⊆ (0...𝑁)) |
39 | 38 | sselda 3603 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ (0...𝑁)) |
40 | 39, 16 | syldan 487 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁C𝑘) · (𝐴↑𝑘)) ∈ ℂ) |
41 | 31, 40 | fsumcl 14464 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ Σ𝑘 ∈
(0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) ∈ ℂ) |
42 | 41, 24 | pncand 10393 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((Σ𝑘 ∈
(0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) + (𝐴↑𝑁)) − (𝐴↑𝑁)) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘))) |
43 | 30, 42 | eqtrd 2656 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (((𝐴 + 1)↑𝑁) − (𝐴↑𝑁)) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘))) |