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

Metamath Proof Explorer

Theorem 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 ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ≠ 0 )

Proof

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