This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem binom1p

Description: Special case of the binomial theorem for ( 1 + A ) ^ N . (Contributed by Paul Chapman, 10-May-2007)

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

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 binom ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 1 + 𝐴 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐴 ↑ 𝑘 ) ) ) )
3 1 2 mp3an1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 1 + 𝐴 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐴 ↑ 𝑘 ) ) ) )
4 fznn0sub ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 )
5 4 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 )
6 5 nn0zd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝑘 ) ∈ ℤ )
7 1exp ⊢ ( ( 𝑁 − 𝑘 ) ∈ ℤ → ( 1 ↑ ( 𝑁 − 𝑘 ) ) = 1 )
8 6 7 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 1 ↑ ( 𝑁 − 𝑘 ) ) = 1 )
9 8 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐴 ↑ 𝑘 ) ) = ( 1 · ( 𝐴 ↑ 𝑘 ) ) )
10 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
11 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
12 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
13 10 11 12 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
14 13 mullidd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 1 · ( 𝐴 ↑ 𝑘 ) ) = ( 𝐴 ↑ 𝑘 ) )
15 9 14 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐴 ↑ 𝑘 ) ) = ( 𝐴 ↑ 𝑘 ) )
16 15 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( ( 𝑁 C 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )
17 16 sumeq2dv ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐴 ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )
18 3 17 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 1 + 𝐴 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )