Theorem efneg

Description: The exponential of the opposite is the inverse of the exponential. (Contributed by Mario Carneiro, 10-May-2014)

	Ref	Expression
Assertion	efneg	$$⊢A\in ℂ\to {\mathrm{e}}^{-A}=\frac{1}{{\mathrm{e}}^A}$$

Proof

Step	Hyp	Ref	Expression
1		efcl	$$⊢A\in ℂ\to {\mathrm{e}}^A\in ℂ$$
2		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
3		efcl	$$⊢-A\in ℂ\to {\mathrm{e}}^{-A}\in ℂ$$
4	2 3	syl	$$⊢A\in ℂ\to {\mathrm{e}}^{-A}\in ℂ$$
5		efne0	$$⊢A\in ℂ\to {\mathrm{e}}^A\ne 0$$
6		efcan	$$⊢A\in ℂ\to {\mathrm{e}}^A{\mathrm{e}}^{-A}=1$$
7	1 4 5 6	mvllmuld	$$⊢A\in ℂ\to {\mathrm{e}}^{-A}=\frac{1}{{\mathrm{e}}^A}$$