efne0OLD

Description: Obsolete version of efne0 as of 14-Nov-2025. 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) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	efne0OLD	$⊢ A \in ℂ \to e^{A} \neq 0$

Proof

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

Metamath Proof Explorer

Theorem efne0OLD

Proof