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 ( 𝐴 ∈ ℂ → ( ( exp ‘ 𝐴 ) · ( exp ‘ - 𝐴 ) ) = 1 )

Proof

Step Hyp Ref Expression
1 negcl ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
2 efadd ( ( 𝐴 ∈ ℂ ∧ - 𝐴 ∈ ℂ ) → ( exp ‘ ( 𝐴 + - 𝐴 ) ) = ( ( exp ‘ 𝐴 ) · ( exp ‘ - 𝐴 ) ) )
3 1 2 mpdan ( 𝐴 ∈ ℂ → ( exp ‘ ( 𝐴 + - 𝐴 ) ) = ( ( exp ‘ 𝐴 ) · ( exp ‘ - 𝐴 ) ) )
4 negid ( 𝐴 ∈ ℂ → ( 𝐴 + - 𝐴 ) = 0 )
5 4 fveq2d ( 𝐴 ∈ ℂ → ( exp ‘ ( 𝐴 + - 𝐴 ) ) = ( exp ‘ 0 ) )
6 ef0 ( exp ‘ 0 ) = 1
7 5 6 eqtrdi ( 𝐴 ∈ ℂ → ( exp ‘ ( 𝐴 + - 𝐴 ) ) = 1 )
8 3 7 eqtr3d ( 𝐴 ∈ ℂ → ( ( exp ‘ 𝐴 ) · ( exp ‘ - 𝐴 ) ) = 1 )