Metamath Proof Explorer


Theorem plpv

Description: Value of addition on positive reals. (Contributed by NM, 28-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion plpv A𝑷B𝑷A+𝑷B=x|yAzBx=y+𝑸z

Proof

Step Hyp Ref Expression
1 df-plp +𝑷=u𝑷,v𝑷f|guhvf=g+𝑸h
2 addclnq g𝑸h𝑸g+𝑸h𝑸
3 1 2 genpv A𝑷B𝑷A+𝑷B=x|yAzBx=y+𝑸z