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 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2nn0 | ⊢ 2 ∈ ℕ0 | |
2 | nn0expcl | ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) → ( 𝐴 ↑ 2 ) ∈ ℕ0 ) | |
3 | 1 2 | mpan2 | ⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 ↑ 2 ) ∈ ℕ0 ) |