Metamath Proof Explorer


Theorem resqcli

Description: Closure of square in reals. (Contributed by NM, 2-Aug-1999)

Ref Expression
Hypothesis resqcl.1 ⊢ A ∈ ℝ
Assertion resqcli ⊢ A 2 ∈ ℝ

Proof

Step Hyp Ref Expression
1 resqcl.1 ⊢ A ∈ ℝ
2 resqcl ⊢ A ∈ ℝ → A 2 ∈ ℝ
3 1 2 ax-mp ⊢ A 2 ∈ ℝ