Metamath Proof Explorer


Theorem addasspr

Description: Addition of positive reals is associative. Proposition 9-3.5(i) of Gleason p. 123. (Contributed by NM, 18-Mar-1996) (New usage is discouraged.)

Ref Expression
Assertion addasspr
|- ( ( A +P. B ) +P. C ) = ( A +P. ( B +P. C ) )

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 dmplp
 |-  dom +P. = ( P. X. P. )
4 addclpr
 |-  ( ( f e. P. /\ g e. P. ) -> ( f +P. g ) e. P. )
5 addassnq
 |-  ( ( f +Q g ) +Q h ) = ( f +Q ( g +Q h ) )
6 1 2 3 4 5 genpass
 |-  ( ( A +P. B ) +P. C ) = ( A +P. ( B +P. C ) )