Metamath Proof Explorer


Theorem resqcli

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

Ref Expression
Hypothesis resqcl.1
|- A e. RR
Assertion resqcli
|- ( A ^ 2 ) e. RR

Proof

Step Hyp Ref Expression
1 resqcl.1
 |-  A e. RR
2 resqcl
 |-  ( A e. RR -> ( A ^ 2 ) e. RR )
3 1 2 ax-mp
 |-  ( A ^ 2 ) e. RR