Metamath Proof Explorer

Theorem expne0i

Description: Nonnegative integer exponentiation is nonzero if its base is nonzero. (Contributed by NM, 2-Aug-2006) (Revised by Mario Carneiro, 4-Jun-2014)

		Ref	Expression
	Assertion	expne0i	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N} \neq 0$

Proof

Step	Hyp	Ref	Expression
1		expclzlem	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N} \in (ℂ ∖ \{0\})$
2		eldifsni	$⊢ A^{N} \in (ℂ ∖ \{0\}) \to A^{N} \neq 0$
3	1 2	syl	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N} \neq 0$