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 φ A
Assertion efne0d φ e A 0

Proof

Step Hyp Ref Expression
1 efne0d.1 φ A
2 ax-1ne0 1 0
3 oveq1 e A = 0 e A e A = 0 e A
4 efcan A e A e A = 1
5 1 4 syl φ e A e A = 1
6 1 negcld φ A
7 6 efcld φ e A
8 7 mul02d φ 0 e A = 0
9 5 8 eqeq12d φ e A e A = 0 e A 1 = 0
10 3 9 imbitrid φ e A = 0 1 = 0
11 10 necon3d φ 1 0 e A 0
12 2 11 mpi φ e A 0