This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem addcomnq

Description: Addition of positive fractions is commutative. (Contributed by NM, 30-Aug-1995) (Revised by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion addcomnq 
|- ( A +Q B ) = ( B +Q A )

Proof

Step Hyp Ref Expression
1 addcompq 
 |-  ( A +pQ B ) = ( B +pQ A )
2 1 fveq2i 
 |-  ( /Q ` ( A +pQ B ) ) = ( /Q ` ( B +pQ A ) )
3 addpqnq 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A +Q B ) = ( /Q ` ( A +pQ B ) ) )
4 addpqnq 
 |-  ( ( B e. Q. /\ A e. Q. ) -> ( B +Q A ) = ( /Q ` ( B +pQ A ) ) )
5 4 ancoms 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( B +Q A ) = ( /Q ` ( B +pQ A ) ) )
6 2 3 5 3eqtr4a 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A +Q B ) = ( B +Q A ) )
7 addnqf 
 |-  +Q : ( Q. X. Q. ) --> Q.
8 7 fdmi 
 |-  dom +Q = ( Q. X. Q. )
9 8 ndmovcom 
 |-  ( -. ( A e. Q. /\ B e. Q. ) -> ( A +Q B ) = ( B +Q A ) )
10 6 9 pm2.61i 
 |-  ( A +Q B ) = ( B +Q A )