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 )