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 
|- ( ( 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 ) ) ) ) )