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\in ℂ\to {\mathrm{e}}^A{\mathrm{e}}^{-A}=1$$

Proof

Step	Hyp	Ref	Expression
1		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
2		efadd	$$⊢\left(A\in ℂ\wedge -A\in ℂ\right)\to {\mathrm{e}}^{A+\left(-A\right)}={\mathrm{e}}^A{\mathrm{e}}^{-A}$$
3	1 2	mpdan	$$⊢A\in ℂ\to {\mathrm{e}}^{A+\left(-A\right)}={\mathrm{e}}^A{\mathrm{e}}^{-A}$$
4		negid	$$⊢A\in ℂ\to A+\left(-A\right)=0$$
5	4	fveq2d	$$⊢A\in ℂ\to {\mathrm{e}}^{A+\left(-A\right)}={\mathrm{e}}^0$$
6		ef0	$$⊢{\mathrm{e}}^0=1$$
7	5 6	eqtrdi	$$⊢A\in ℂ\to {\mathrm{e}}^{A+\left(-A\right)}=1$$
8	3 7	eqtr3d	$$⊢A\in ℂ\to {\mathrm{e}}^A{\mathrm{e}}^{-A}=1$$