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