Theorem nn0expcl

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

	Ref	Expression
Assertion	nn0expcl	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		nn0sscn	⊢ ℕ0 ⊆ ℂ
2		nn0mulcl	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 · 𝑦 ) ∈ ℕ0 )
3		1nn0	⊢ 1 ∈ ℕ0
4	1 2 3	expcllem	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℕ0 )