Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
Integer powers
resqcli
Next ⟩
sqgt0i
Metamath Proof Explorer
Ascii
Unicode
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
∈
ℝ