Metamath Proof Explorer


Theorem rpreccl

Description: Closure law for reciprocation of positive reals. (Contributed by Jeff Hankins, 23-Nov-2008)

Ref Expression
Assertion rpreccl A + 1 A +

Proof

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