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