Metamath Proof Explorer


Theorem efneg

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

Proof

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