Metamath Proof Explorer


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 )