Metamath Proof Explorer


Theorem zexpcl

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

Ref Expression
Assertion zexpcl ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴𝑁 ) ∈ ℤ )

Proof

Step Hyp Ref Expression
1 zsscn ℤ ⊆ ℂ
2 zmulcl ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
3 1z 1 ∈ ℤ
4 1 2 3 expcllem ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴𝑁 ) ∈ ℤ )