Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
Integer powers
resqcld
Next ⟩
sqge0d
Metamath Proof Explorer
Ascii
Unicode
Theorem
resqcld
Description:
Closure of square in reals.
(Contributed by
Mario Carneiro
, 28-May-2016)
Ref
Expression
Hypothesis
resqcld.1
⊢
φ
→
A
∈
ℝ
Assertion
resqcld
⊢
φ
→
A
2
∈
ℝ
Proof
Step
Hyp
Ref
Expression
1
resqcld.1
⊢
φ
→
A
∈
ℝ
2
resqcl
⊢
A
∈
ℝ
→
A
2
∈
ℝ
3
1
2
syl
⊢
φ
→
A
2
∈
ℝ