Metamath Proof Explorer


Theorem mulcomnq

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

Ref Expression
Assertion mulcomnq A𝑸B=B𝑸A

Proof

Step Hyp Ref Expression
1 mulcompq A𝑝𝑸B=B𝑝𝑸A
2 1 fveq2i /𝑸A𝑝𝑸B=/𝑸B𝑝𝑸A
3 mulpqnq A𝑸B𝑸A𝑸B=/𝑸A𝑝𝑸B
4 mulpqnq B𝑸A𝑸B𝑸A=/𝑸B𝑝𝑸A
5 4 ancoms A𝑸B𝑸B𝑸A=/𝑸B𝑝𝑸A
6 2 3 5 3eqtr4a A𝑸B𝑸A𝑸B=B𝑸A
7 mulnqf 𝑸:𝑸×𝑸𝑸
8 7 fdmi dom𝑸=𝑸×𝑸
9 8 ndmovcom ¬A𝑸B𝑸A𝑸B=B𝑸A
10 6 9 pm2.61i A𝑸B=B𝑸A