Step |
Hyp |
Ref |
Expression |
1 |
|
negcl |
|- ( A e. CC -> -u A e. CC ) |
2 |
|
efadd |
|- ( ( A e. CC /\ -u A e. CC ) -> ( exp ` ( A + -u A ) ) = ( ( exp ` A ) x. ( exp ` -u A ) ) ) |
3 |
1 2
|
mpdan |
|- ( A e. CC -> ( exp ` ( A + -u A ) ) = ( ( exp ` A ) x. ( exp ` -u A ) ) ) |
4 |
|
negid |
|- ( A e. CC -> ( A + -u A ) = 0 ) |
5 |
4
|
fveq2d |
|- ( A e. CC -> ( exp ` ( A + -u A ) ) = ( exp ` 0 ) ) |
6 |
|
ef0 |
|- ( exp ` 0 ) = 1 |
7 |
5 6
|
eqtrdi |
|- ( A e. CC -> ( exp ` ( A + -u A ) ) = 1 ) |
8 |
3 7
|
eqtr3d |
|- ( A e. CC -> ( ( exp ` A ) x. ( exp ` -u A ) ) = 1 ) |