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