Theorem expclz

Description: Closure law for integer exponentiation of complex numnbers. (Contributed by Mario Carneiro, 4-Jun-2014)

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

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	1	eldifad	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge N\in \mathbb{Z}\right)\to A^N\in ℂ$$