This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efne0d

Description: The exponential of a complex number is nonzero, deduction form. (Contributed by NM, 13-Jan-2006) (Revised by Mario Carneiro, 29-Apr-2014) (Revised by SN, 25-Apr-2025)

		Ref	Expression
	Hypothesis	efne0d.1	$⊢ φ \to A \in ℂ$
	Assertion	efne0d	$⊢ φ \to e^{A} \neq 0$

Proof

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