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 )