This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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