Metamath Proof Explorer


Theorem expne0d

Description: Nonnegative integer exponentiation is nonzero if its base is nonzero. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses expcld.1 ( 𝜑𝐴 ∈ ℂ )
sqrecd.1 ( 𝜑𝐴 ≠ 0 )
expclzd.3 ( 𝜑𝑁 ∈ ℤ )
Assertion expne0d ( 𝜑 → ( 𝐴𝑁 ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 expcld.1 ( 𝜑𝐴 ∈ ℂ )
2 sqrecd.1 ( 𝜑𝐴 ≠ 0 )
3 expclzd.3 ( 𝜑𝑁 ∈ ℤ )
4 expne0i ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴𝑁 ) ≠ 0 )
5 1 2 3 4 syl3anc ( 𝜑 → ( 𝐴𝑁 ) ≠ 0 )