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

Metamath Proof Explorer

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 ‘ ( 𝑁 · 𝐴 ) ) ) ) )