Theorem expne0

Description: A positive integer power is nonzero if and only if its base is nonzero. (Contributed by NM, 6-May-2005)

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

Proof

Step	Hyp	Ref	Expression
1		expeq0	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to \left(A^N=0\leftrightarrow A=0\right)$$
2	1	necon3bid	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to \left(A^N\ne 0\leftrightarrow A\ne 0\right)$$