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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
Assertion	efne0d	⊢ ( 𝜑 → ( exp ‘ 𝐴 ) ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		efne0d.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		ax-1ne0	⊢ 1 ≠ 0
3		oveq1	⊢ ( ( exp ‘ 𝐴 ) = 0 → ( ( exp ‘ 𝐴 ) · ( exp ‘ - 𝐴 ) ) = ( 0 · ( exp ‘ - 𝐴 ) ) )
4		efcan	⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ 𝐴 ) · ( exp ‘ - 𝐴 ) ) = 1 )
5	1 4	syl	⊢ ( 𝜑 → ( ( exp ‘ 𝐴 ) · ( exp ‘ - 𝐴 ) ) = 1 )
6	1	negcld	⊢ ( 𝜑 → - 𝐴 ∈ ℂ )
7	6	efcld	⊢ ( 𝜑 → ( exp ‘ - 𝐴 ) ∈ ℂ )
8	7	mul02d	⊢ ( 𝜑 → ( 0 · ( exp ‘ - 𝐴 ) ) = 0 )
9	5 8	eqeq12d	⊢ ( 𝜑 → ( ( ( exp ‘ 𝐴 ) · ( exp ‘ - 𝐴 ) ) = ( 0 · ( exp ‘ - 𝐴 ) ) ↔ 1 = 0 ) )
10	3 9	imbitrid	⊢ ( 𝜑 → ( ( exp ‘ 𝐴 ) = 0 → 1 = 0 ) )
11	10	necon3d	⊢ ( 𝜑 → ( 1 ≠ 0 → ( exp ‘ 𝐴 ) ≠ 0 ) )
12	2 11	mpi	⊢ ( 𝜑 → ( exp ‘ 𝐴 ) ≠ 0 )