Metamath Proof Explorer

Theorem efcan

Description: Cancellation law for exponential function. Equation 27 of Rudin p. 164. (Contributed by NM, 13-Jan-2006)

Ref Expression
Assertion efcan 
|- ( A e. CC -> ( ( exp ` A ) x. ( exp ` -u A ) ) = 1 )

Proof

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 )