Metamath Proof Explorer


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 )