Metamath Proof Explorer

Theorem binom1dif

Description: A summation for the difference between ( ( A + 1 ) ^ N ) and ( A ^ N ) . (Contributed by Scott Fenton, 9-Apr-2014) (Revised by Mario Carneiro, 22-May-2014)

Ref Expression
Assertion binom1dif ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐴 + 1 ) ↑ 𝑁 ) − ( 𝐴 ↑ 𝑁 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 fzfid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin )
2 fzssp1 ⊢ ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... ( ( 𝑁 − 1 ) + 1 ) )
3 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
4 3 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
5 ax-1cn ⊢ 1 ∈ ℂ
6 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
7 4 5 6 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
8 7 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 0 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 0 ... 𝑁 ) )
9 2 8 sseqtrid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
10 9 sselda ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
11 bccl2 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝑘 ) ∈ ℕ )
12 11 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑘 ) ∈ ℕ )
13 12 nncnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑘 ) ∈ ℂ )
14 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
15 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
16 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
17 14 15 16 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
18 13 17 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ )
19 10 18 syldan ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ )
20 1 19 fsumcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ )
21 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
22 addcom ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 + 1 ) = ( 1 + 𝐴 ) )
23 14 5 22 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 + 1 ) = ( 1 + 𝐴 ) )
24 23 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 + 1 ) ↑ 𝑁 ) = ( ( 1 + 𝐴 ) ↑ 𝑁 ) )
25 binom1p ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 1 + 𝐴 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )
26 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
27 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
28 26 27 eleqtrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
29 oveq2 ⊢ ( 𝑘 = 𝑁 → ( 𝑁 C 𝑘 ) = ( 𝑁 C 𝑁 ) )
30 oveq2 ⊢ ( 𝑘 = 𝑁 → ( 𝐴 ↑ 𝑘 ) = ( 𝐴 ↑ 𝑁 ) )
31 29 30 oveq12d ⊢ ( 𝑘 = 𝑁 → ( ( 𝑁 C 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) = ( ( 𝑁 C 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) )
32 28 18 31 fsumm1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( 𝑁 C 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) )
33 bcnn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 𝑁 ) = 1 )
34 33 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 C 𝑁 ) = 1 )
35 34 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 C 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) = ( 1 · ( 𝐴 ↑ 𝑁 ) ) )
36 21 mulid2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 1 · ( 𝐴 ↑ 𝑁 ) ) = ( 𝐴 ↑ 𝑁 ) )
37 35 36 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 C 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) = ( 𝐴 ↑ 𝑁 ) )
38 37 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) + ( ( 𝑁 C 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) + ( 𝐴 ↑ 𝑁 ) ) )
39 32 38 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) + ( 𝐴 ↑ 𝑁 ) ) )
40 24 25 39 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 + 1 ) ↑ 𝑁 ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) + ( 𝐴 ↑ 𝑁 ) ) )
41 20 21 40 mvrraddd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐴 + 1 ) ↑ 𝑁 ) − ( 𝐴 ↑ 𝑁 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )