Metamath Proof Explorer


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 )