Metamath Proof Explorer


Theorem mulpipq

Description: Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

Ref Expression
Assertion mulpipq A𝑵B𝑵C𝑵D𝑵AB𝑝𝑸CD=A𝑵CB𝑵D

Proof

Step Hyp Ref Expression
1 opelxpi A𝑵B𝑵AB𝑵×𝑵
2 opelxpi C𝑵D𝑵CD𝑵×𝑵
3 mulpipq2 AB𝑵×𝑵CD𝑵×𝑵AB𝑝𝑸CD=1stAB𝑵1stCD2ndAB𝑵2ndCD
4 1 2 3 syl2an A𝑵B𝑵C𝑵D𝑵AB𝑝𝑸CD=1stAB𝑵1stCD2ndAB𝑵2ndCD
5 op1stg A𝑵B𝑵1stAB=A
6 op1stg C𝑵D𝑵1stCD=C
7 5 6 oveqan12d A𝑵B𝑵C𝑵D𝑵1stAB𝑵1stCD=A𝑵C
8 op2ndg A𝑵B𝑵2ndAB=B
9 op2ndg C𝑵D𝑵2ndCD=D
10 8 9 oveqan12d A𝑵B𝑵C𝑵D𝑵2ndAB𝑵2ndCD=B𝑵D
11 7 10 opeq12d A𝑵B𝑵C𝑵D𝑵1stAB𝑵1stCD2ndAB𝑵2ndCD=A𝑵CB𝑵D
12 4 11 eqtrd A𝑵B𝑵C𝑵D𝑵AB𝑝𝑸CD=A𝑵CB𝑵D