Metamath Proof Explorer


Theorem rphalfcl

Description: Closure law for half of a positive real. (Contributed by Mario Carneiro, 31-Jan-2014)

Ref Expression
Assertion rphalfcl A + A 2 +

Proof

Step Hyp Ref Expression
1 2rp 2 +
2 rpdivcl A + 2 + A 2 +
3 1 2 mpan2 A + A 2 +