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	mulid2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ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 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )