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
|- ( ( A e. CC /\ N e. ZZ ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ^ N ) = ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ax-icn
 |-  _i e. CC
2 mulcl
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
3 1 2 mpan
 |-  ( A e. CC -> ( _i x. A ) e. CC )
4 efexp
 |-  ( ( ( _i x. A ) e. CC /\ N e. ZZ ) -> ( exp ` ( N x. ( _i x. A ) ) ) = ( ( exp ` ( _i x. A ) ) ^ N ) )
5 3 4 sylan
 |-  ( ( A e. CC /\ N e. ZZ ) -> ( exp ` ( N x. ( _i x. A ) ) ) = ( ( exp ` ( _i x. A ) ) ^ N ) )
6 zcn
 |-  ( N e. ZZ -> N e. CC )
7 mul12
 |-  ( ( N e. CC /\ _i e. CC /\ A e. CC ) -> ( N x. ( _i x. A ) ) = ( _i x. ( N x. A ) ) )
8 1 7 mp3an2
 |-  ( ( N e. CC /\ A e. CC ) -> ( N x. ( _i x. A ) ) = ( _i x. ( N x. A ) ) )
9 8 fveq2d
 |-  ( ( N e. CC /\ A e. CC ) -> ( exp ` ( N x. ( _i x. A ) ) ) = ( exp ` ( _i x. ( N x. A ) ) ) )
10 mulcl
 |-  ( ( N e. CC /\ A e. CC ) -> ( N x. A ) e. CC )
11 efival
 |-  ( ( N x. A ) e. CC -> ( exp ` ( _i x. ( N x. A ) ) ) = ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) )
12 10 11 syl
 |-  ( ( N e. CC /\ A e. CC ) -> ( exp ` ( _i x. ( N x. A ) ) ) = ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) )
13 9 12 eqtrd
 |-  ( ( N e. CC /\ A e. CC ) -> ( exp ` ( N x. ( _i x. A ) ) ) = ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) )
14 13 ancoms
 |-  ( ( A e. CC /\ N e. CC ) -> ( exp ` ( N x. ( _i x. A ) ) ) = ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) )
15 6 14 sylan2
 |-  ( ( A e. CC /\ N e. ZZ ) -> ( exp ` ( N x. ( _i x. A ) ) ) = ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) )
16 efival
 |-  ( A e. CC -> ( exp ` ( _i x. A ) ) = ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) )
17 16 oveq1d
 |-  ( A e. CC -> ( ( exp ` ( _i x. A ) ) ^ N ) = ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ^ N ) )
18 17 adantr
 |-  ( ( A e. CC /\ N e. ZZ ) -> ( ( exp ` ( _i x. A ) ) ^ N ) = ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ^ N ) )
19 5 15 18 3eqtr3rd
 |-  ( ( A e. CC /\ N e. ZZ ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ^ N ) = ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) )