Metamath Proof Explorer


Theorem resqcl

Description: Closure of the square of a real number. (Contributed by NM, 18-Oct-1999)

Ref Expression
Assertion resqcl A A 2

Proof

Step Hyp Ref Expression
1 2nn0 2 0
2 reexpcl A 2 0 A 2
3 1 2 mpan2 A A 2