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 )