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