Theorem nn0sqcl

Description: The square of a nonnegative integer is a nonnegative integer. (Contributed by Stefan O'Rear, 16-Oct-2014)

	Ref	Expression
Assertion	nn0sqcl	⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 ↑ 2 ) ∈ ℕ0 )

Proof

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