Theorem efne0d

Description: The exponential of a complex number is nonzero, deduction form. EDITORIAL: Using efne0d in efne0 is shorter than vice versa. (Contributed by SN, 25-Apr-2025)

	Ref	Expression
Hypothesis	efne0d.1	$$⊢\phi \to A\in ℂ$$
Assertion	efne0d	$$⊢\phi \to {\mathrm{e}}^A\ne 0$$

Proof

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