Metamath Proof Explorer


Theorem addpipq

Description: Addition of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

Ref Expression
Assertion addpipq A𝑵B𝑵C𝑵D𝑵AB+𝑝𝑸CD=A𝑵D+𝑵C𝑵BB𝑵D

Proof

Step Hyp Ref Expression
1 opelxpi A𝑵B𝑵AB𝑵×𝑵
2 opelxpi C𝑵D𝑵CD𝑵×𝑵
3 addpipq2 AB𝑵×𝑵CD𝑵×𝑵AB+𝑝𝑸CD=1stAB𝑵2ndCD+𝑵1stCD𝑵2ndAB2ndAB𝑵2ndCD
4 1 2 3 syl2an A𝑵B𝑵C𝑵D𝑵AB+𝑝𝑸CD=1stAB𝑵2ndCD+𝑵1stCD𝑵2ndAB2ndAB𝑵2ndCD
5 op1stg A𝑵B𝑵1stAB=A
6 op2ndg C𝑵D𝑵2ndCD=D
7 5 6 oveqan12d A𝑵B𝑵C𝑵D𝑵1stAB𝑵2ndCD=A𝑵D
8 op1stg C𝑵D𝑵1stCD=C
9 op2ndg A𝑵B𝑵2ndAB=B
10 8 9 oveqan12rd A𝑵B𝑵C𝑵D𝑵1stCD𝑵2ndAB=C𝑵B
11 7 10 oveq12d A𝑵B𝑵C𝑵D𝑵1stAB𝑵2ndCD+𝑵1stCD𝑵2ndAB=A𝑵D+𝑵C𝑵B
12 9 6 oveqan12d A𝑵B𝑵C𝑵D𝑵2ndAB𝑵2ndCD=B𝑵D
13 11 12 opeq12d A𝑵B𝑵C𝑵D𝑵1stAB𝑵2ndCD+𝑵1stCD𝑵2ndAB2ndAB𝑵2ndCD=A𝑵D+𝑵C𝑵BB𝑵D
14 4 13 eqtrd A𝑵B𝑵C𝑵D𝑵AB+𝑝𝑸CD=A𝑵D+𝑵C𝑵BB𝑵D