Theorem nn0expcl

Description: Closure of exponentiation of nonnegative integers. (Contributed by NM, 14-Dec-2005)

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

Proof

Step	Hyp	Ref	Expression
1		nn0sscn	$$⊢{\mathbb{N}}_0\subseteq ℂ$$
2		nn0mulcl	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to xy\in {\mathbb{N}}_0$$
3		1nn0	$$⊢1\in {\mathbb{N}}_0$$
4	1 2 3	expcllem	$$⊢\left(A\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to A^N\in {\mathbb{N}}_0$$