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 ) ∈ ℤ )