Proof of Theorem binom1dif
Step | Hyp | Ref
| Expression |
1 | | 0zd 9224 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 0 ∈ ℤ) |
2 | | simpr 109 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℕ0) |
3 | 2 | nn0zd 9332 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℤ) |
4 | | peano2zm 9250 |
. . . . 5
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
5 | 3, 4 | syl 14 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝑁 − 1) ∈
ℤ) |
6 | 1, 5 | fzfigd 10387 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (0...(𝑁 − 1))
∈ Fin) |
7 | | fzssp1 10023 |
. . . . . 6
⊢
(0...(𝑁 − 1))
⊆ (0...((𝑁 − 1)
+ 1)) |
8 | | nn0cn 9145 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
9 | 8 | adantl 275 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℂ) |
10 | | ax-1cn 7867 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
11 | | npcan 8128 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
12 | 9, 10, 11 | sylancl 411 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝑁 − 1) + 1)
= 𝑁) |
13 | 12 | oveq2d 5869 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (0...((𝑁 − 1)
+ 1)) = (0...𝑁)) |
14 | 7, 13 | sseqtrid 3197 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (0...(𝑁 − 1))
⊆ (0...𝑁)) |
15 | 14 | sselda 3147 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ (0...𝑁)) |
16 | | bccl2 10702 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑁) → (𝑁C𝑘) ∈ ℕ) |
17 | 16 | adantl 275 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈ ℕ) |
18 | 17 | nncnd 8892 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈ ℂ) |
19 | | simpl 108 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝐴 ∈
ℂ) |
20 | | elfznn0 10070 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
21 | | expcl 10494 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℂ) |
22 | 19, 20, 21 | syl2an 287 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → (𝐴↑𝑘) ∈ ℂ) |
23 | 18, 22 | mulcld 7940 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · (𝐴↑𝑘)) ∈ ℂ) |
24 | 15, 23 | syldan 280 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁C𝑘) · (𝐴↑𝑘)) ∈ ℂ) |
25 | 6, 24 | fsumcl 11363 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ Σ𝑘 ∈
(0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) ∈ ℂ) |
26 | | expcl 10494 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝐴↑𝑁) ∈
ℂ) |
27 | | addcom 8056 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 + 1) =
(1 + 𝐴)) |
28 | 19, 10, 27 | sylancl 411 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝐴 + 1) = (1 + 𝐴)) |
29 | 28 | oveq1d 5868 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 + 1)↑𝑁) = ((1 + 𝐴)↑𝑁)) |
30 | | binom1p 11448 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((1 + 𝐴)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · (𝐴↑𝑘))) |
31 | | nn0uz 9521 |
. . . . . 6
⊢
ℕ0 = (ℤ≥‘0) |
32 | 2, 31 | eleqtrdi 2263 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
(ℤ≥‘0)) |
33 | | oveq2 5861 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (𝑁C𝑘) = (𝑁C𝑁)) |
34 | | oveq2 5861 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (𝐴↑𝑘) = (𝐴↑𝑁)) |
35 | 33, 34 | oveq12d 5871 |
. . . . 5
⊢ (𝑘 = 𝑁 → ((𝑁C𝑘) · (𝐴↑𝑘)) = ((𝑁C𝑁) · (𝐴↑𝑁))) |
36 | 32, 23, 35 | fsumm1 11379 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ Σ𝑘 ∈
(0...𝑁)((𝑁C𝑘) · (𝐴↑𝑘)) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) + ((𝑁C𝑁) · (𝐴↑𝑁)))) |
37 | | bcnn 10691 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑁C𝑁) = 1) |
38 | 37 | adantl 275 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝑁C𝑁) = 1) |
39 | 38 | oveq1d 5868 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝑁C𝑁) · (𝐴↑𝑁)) = (1 · (𝐴↑𝑁))) |
40 | 26 | mulid2d 7938 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (1 · (𝐴↑𝑁)) = (𝐴↑𝑁)) |
41 | 39, 40 | eqtrd 2203 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝑁C𝑁) · (𝐴↑𝑁)) = (𝐴↑𝑁)) |
42 | 41 | oveq2d 5869 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (Σ𝑘 ∈
(0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) + ((𝑁C𝑁) · (𝐴↑𝑁))) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) + (𝐴↑𝑁))) |
43 | 36, 42 | eqtrd 2203 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ Σ𝑘 ∈
(0...𝑁)((𝑁C𝑘) · (𝐴↑𝑘)) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) + (𝐴↑𝑁))) |
44 | 29, 30, 43 | 3eqtrd 2207 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((𝐴 + 1)↑𝑁) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘)) + (𝐴↑𝑁))) |
45 | 25, 26, 44 | mvrraddd 8285 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (((𝐴 + 1)↑𝑁) − (𝐴↑𝑁)) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · (𝐴↑𝑘))) |