Theorem expcl

Description: Closure law for nonnegative integer exponentiation. For integer exponents, see expclz . (Contributed by NM, 26-May-2005)

	Ref	Expression
Assertion	expcl	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to A^N\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢ℂ\subseteq ℂ$$
2		mulcl	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to xy\in ℂ$$
3		ax-1cn	$$⊢1\in ℂ$$
4	1 2 3	expcllem	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to A^N\in ℂ$$