Theorem demoivre

Description: De Moivre's Formula. Proof by induction given at http://en.wikipedia.org/wiki/De_Moivre's_formula , but restricted to nonnegative integer powers. See also demoivreALT for an alternate longer proof not using the exponential function. (Contributed by NM, 24-Jul-2007)

	Ref	Expression
Assertion	demoivre	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ) → ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) ↑ 𝑁 ) = ( ( cos ‘ ( 𝑁 · 𝐴 ) ) + ( i · ( sin ‘ ( 𝑁 · 𝐴 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax-icn	⊢ i ∈ ℂ
2		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
3	1 2	mpan	⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
4		efexp	⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ 𝑁 ∈ ℤ ) → ( exp ‘ ( 𝑁 · ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) ↑ 𝑁 ) )
5	3 4	sylan	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ) → ( exp ‘ ( 𝑁 · ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) ↑ 𝑁 ) )
6		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
7		mul12	⊢ ( ( 𝑁 ∈ ℂ ∧ i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝑁 · ( i · 𝐴 ) ) = ( i · ( 𝑁 · 𝐴 ) ) )
8	1 7	mp3an2	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝑁 · ( i · 𝐴 ) ) = ( i · ( 𝑁 · 𝐴 ) ) )
9	8	fveq2d	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( exp ‘ ( 𝑁 · ( i · 𝐴 ) ) ) = ( exp ‘ ( i · ( 𝑁 · 𝐴 ) ) ) )
10		mulcl	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝑁 · 𝐴 ) ∈ ℂ )
11		efival	⊢ ( ( 𝑁 · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · ( 𝑁 · 𝐴 ) ) ) = ( ( cos ‘ ( 𝑁 · 𝐴 ) ) + ( i · ( sin ‘ ( 𝑁 · 𝐴 ) ) ) ) )
12	10 11	syl	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( exp ‘ ( i · ( 𝑁 · 𝐴 ) ) ) = ( ( cos ‘ ( 𝑁 · 𝐴 ) ) + ( i · ( sin ‘ ( 𝑁 · 𝐴 ) ) ) ) )
13	9 12	eqtrd	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( exp ‘ ( 𝑁 · ( i · 𝐴 ) ) ) = ( ( cos ‘ ( 𝑁 · 𝐴 ) ) + ( i · ( sin ‘ ( 𝑁 · 𝐴 ) ) ) ) )
14	13	ancoms	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( exp ‘ ( 𝑁 · ( i · 𝐴 ) ) ) = ( ( cos ‘ ( 𝑁 · 𝐴 ) ) + ( i · ( sin ‘ ( 𝑁 · 𝐴 ) ) ) ) )
15	6 14	sylan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ) → ( exp ‘ ( 𝑁 · ( i · 𝐴 ) ) ) = ( ( cos ‘ ( 𝑁 · 𝐴 ) ) + ( i · ( sin ‘ ( 𝑁 · 𝐴 ) ) ) ) )
16		efival	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) )
17	16	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) ↑ 𝑁 ) = ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) ↑ 𝑁 ) )
18	17	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ) → ( ( exp ‘ ( i · 𝐴 ) ) ↑ 𝑁 ) = ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) ↑ 𝑁 ) )
19	5 15 18	3eqtr3rd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ) → ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) ↑ 𝑁 ) = ( ( cos ‘ ( 𝑁 · 𝐴 ) ) + ( i · ( sin ‘ ( 𝑁 · 𝐴 ) ) ) ) )