Metamath Proof Explorer


Theorem addclpr

Description: Closure of addition on positive reals. First statement of Proposition 9-3.5 of Gleason p. 123. (Contributed by NM, 13-Mar-1996) (New usage is discouraged.)

Ref Expression
Assertion addclpr
|- ( ( A e. P. /\ B e. P. ) -> ( A +P. B ) e. P. )

Proof

Step Hyp Ref Expression
1 df-plp
 |-  +P. = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y +Q z ) } )
2 addclnq
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( y +Q z ) e. Q. )
3 ltanq
 |-  ( h e. Q. -> ( f  ( h +Q f ) 
4 addcomnq
 |-  ( x +Q y ) = ( y +Q x )
5 addclprlem2
 |-  ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x  x e. ( A +P. B ) ) )
6 1 2 3 4 5 genpcl
 |-  ( ( A e. P. /\ B e. P. ) -> ( A +P. B ) e. P. )