Metamath Proof Explorer


Theorem expne0

Description: Positive integer exponentiation is nonzero iff its base is nonzero. (Contributed by NM, 6-May-2005)

Ref Expression
Assertion expne0 ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴𝑁 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )

Proof

Step Hyp Ref Expression
1 expeq0 ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴𝑁 ) = 0 ↔ 𝐴 = 0 ) )
2 1 necon3bid ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴𝑁 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )