Step |
Hyp |
Ref |
Expression |
1 |
|
ax-icn |
|- _i e. CC |
2 |
|
mulneg12 |
|- ( ( _i e. CC /\ A e. CC ) -> ( -u _i x. A ) = ( _i x. -u A ) ) |
3 |
1 2
|
mpan |
|- ( A e. CC -> ( -u _i x. A ) = ( _i x. -u A ) ) |
4 |
3
|
fveq2d |
|- ( A e. CC -> ( exp ` ( -u _i x. A ) ) = ( exp ` ( _i x. -u A ) ) ) |
5 |
|
negcl |
|- ( A e. CC -> -u A e. CC ) |
6 |
|
efival |
|- ( -u A e. CC -> ( exp ` ( _i x. -u A ) ) = ( ( cos ` -u A ) + ( _i x. ( sin ` -u A ) ) ) ) |
7 |
5 6
|
syl |
|- ( A e. CC -> ( exp ` ( _i x. -u A ) ) = ( ( cos ` -u A ) + ( _i x. ( sin ` -u A ) ) ) ) |
8 |
|
cosneg |
|- ( A e. CC -> ( cos ` -u A ) = ( cos ` A ) ) |
9 |
|
sinneg |
|- ( A e. CC -> ( sin ` -u A ) = -u ( sin ` A ) ) |
10 |
9
|
oveq2d |
|- ( A e. CC -> ( _i x. ( sin ` -u A ) ) = ( _i x. -u ( sin ` A ) ) ) |
11 |
|
sincl |
|- ( A e. CC -> ( sin ` A ) e. CC ) |
12 |
|
mulneg2 |
|- ( ( _i e. CC /\ ( sin ` A ) e. CC ) -> ( _i x. -u ( sin ` A ) ) = -u ( _i x. ( sin ` A ) ) ) |
13 |
1 11 12
|
sylancr |
|- ( A e. CC -> ( _i x. -u ( sin ` A ) ) = -u ( _i x. ( sin ` A ) ) ) |
14 |
10 13
|
eqtrd |
|- ( A e. CC -> ( _i x. ( sin ` -u A ) ) = -u ( _i x. ( sin ` A ) ) ) |
15 |
8 14
|
oveq12d |
|- ( A e. CC -> ( ( cos ` -u A ) + ( _i x. ( sin ` -u A ) ) ) = ( ( cos ` A ) + -u ( _i x. ( sin ` A ) ) ) ) |
16 |
|
coscl |
|- ( A e. CC -> ( cos ` A ) e. CC ) |
17 |
|
mulcl |
|- ( ( _i e. CC /\ ( sin ` A ) e. CC ) -> ( _i x. ( sin ` A ) ) e. CC ) |
18 |
1 11 17
|
sylancr |
|- ( A e. CC -> ( _i x. ( sin ` A ) ) e. CC ) |
19 |
16 18
|
negsubd |
|- ( A e. CC -> ( ( cos ` A ) + -u ( _i x. ( sin ` A ) ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) ) |
20 |
15 19
|
eqtrd |
|- ( A e. CC -> ( ( cos ` -u A ) + ( _i x. ( sin ` -u A ) ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) ) |
21 |
7 20
|
eqtrd |
|- ( A e. CC -> ( exp ` ( _i x. -u A ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) ) |
22 |
4 21
|
eqtrd |
|- ( A e. CC -> ( exp ` ( -u _i x. A ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) ) |