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 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℤ )