Description: The exponential of the opposite is the inverse of the exponential. (Contributed by Mario Carneiro, 10-May-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | efneg | |- ( A e. CC -> ( exp ` -u A ) = ( 1 / ( exp ` A ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | efcl | |- ( A e. CC -> ( exp ` A ) e. CC ) |
|
2 | negcl | |- ( A e. CC -> -u A e. CC ) |
|
3 | efcl | |- ( -u A e. CC -> ( exp ` -u A ) e. CC ) |
|
4 | 2 3 | syl | |- ( A e. CC -> ( exp ` -u A ) e. CC ) |
5 | efne0 | |- ( A e. CC -> ( exp ` A ) =/= 0 ) |
|
6 | efcan | |- ( A e. CC -> ( ( exp ` A ) x. ( exp ` -u A ) ) = 1 ) |
|
7 | 1 4 5 6 | mvllmuld | |- ( A e. CC -> ( exp ` -u A ) = ( 1 / ( exp ` A ) ) ) |