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 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
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 )