Metamath Proof Explorer


Theorem resqcl

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

Ref Expression
Assertion resqcl AA2

Proof

Step Hyp Ref Expression
1 2nn0 20
2 reexpcl A20A2
3 1 2 mpan2 AA2