Theorem expne0i

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

	Ref	Expression
Assertion	expne0i	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge N\in \mathbb{Z}\right)\to A^N\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		expclzlem	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge N\in \mathbb{Z}\right)\to A^N\in \left(ℂ\setminus \left\{0\right\}\right)$$
2		eldifsni	$$⊢A^N\in \left(ℂ\setminus \left\{0\right\}\right)\to A^N\ne 0$$
3	1 2	syl	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge N\in \mathbb{Z}\right)\to A^N\ne 0$$