Description: Closure of exponentiation of nonnegative integers. (Contributed by NM, 14-Dec-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | nn0expcl | ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℕ0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0sscn | ⊢ ℕ0 ⊆ ℂ | |
2 | nn0mulcl | ⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 · 𝑦 ) ∈ ℕ0 ) | |
3 | 1nn0 | ⊢ 1 ∈ ℕ0 | |
4 | 1 2 3 | expcllem | ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℕ0 ) |