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

Metamath Proof Explorer

Theorem zsqcl

Description: Integers are closed under squaring. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion zsqcl ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℤ )

Proof

Step Hyp Ref Expression
1 2nn0 ⊢ 2 ∈ ℕ0
2 zexpcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 2 ∈ ℕ0 ) → ( 𝐴 ↑ 2 ) ∈ ℤ )
3 1 2 mpan2 ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℤ )