Theorem efne0

Description: The exponential of a complex number is nonzero. Corollary 15-4.3 of Gleason p. 309. (Contributed by NM, 13-Jan-2006) (Revised by Mario Carneiro, 29-Apr-2014)

	Ref	Expression
Assertion	efne0	$$⊢A\in ℂ\to {\mathrm{e}}^A\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		ax-1ne0	$$⊢1\ne 0$$
2		oveq1	$$⊢{\mathrm{e}}^A=0\to {\mathrm{e}}^A{\mathrm{e}}^{-A}=0\cdot {\mathrm{e}}^{-A}$$
3		efcan	$$⊢A\in ℂ\to {\mathrm{e}}^A{\mathrm{e}}^{-A}=1$$
4		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
5		efcl	$$⊢-A\in ℂ\to {\mathrm{e}}^{-A}\in ℂ$$
6	4 5	syl	$$⊢A\in ℂ\to {\mathrm{e}}^{-A}\in ℂ$$
7	6	mul02d	$$⊢A\in ℂ\to 0\cdot {\mathrm{e}}^{-A}=0$$
8	3 7	eqeq12d	$$⊢A\in ℂ\to \left({\mathrm{e}}^A{\mathrm{e}}^{-A}=0\cdot {\mathrm{e}}^{-A}\leftrightarrow 1=0\right)$$
9	2 8	imbitrid	$$⊢A\in ℂ\to \left({\mathrm{e}}^A=0\to 1=0\right)$$
10	9	necon3d	$$⊢A\in ℂ\to \left(1\ne 0\to {\mathrm{e}}^A\ne 0\right)$$
11	1 10	mpi	$$⊢A\in ℂ\to {\mathrm{e}}^A\ne 0$$