Metamath Proof Explorer


Theorem addpqnq

Description: Addition of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995) (Revised by Mario Carneiro, 26-Dec-2014) (New usage is discouraged.)

Ref Expression
Assertion addpqnq A𝑸B𝑸A+𝑸B=/𝑸A+𝑝𝑸B

Proof

Step Hyp Ref Expression
1 df-plq +𝑸=/𝑸+𝑝𝑸𝑸×𝑸
2 1 fveq1i +𝑸AB=/𝑸+𝑝𝑸𝑸×𝑸AB
3 2 a1i A𝑸B𝑸+𝑸AB=/𝑸+𝑝𝑸𝑸×𝑸AB
4 opelxpi A𝑸B𝑸AB𝑸×𝑸
5 4 fvresd A𝑸B𝑸/𝑸+𝑝𝑸𝑸×𝑸AB=/𝑸+𝑝𝑸AB
6 df-plpq +𝑝𝑸=x𝑵×𝑵,y𝑵×𝑵1stx𝑵2ndy+𝑵1sty𝑵2ndx2ndx𝑵2ndy
7 opex 1stx𝑵2ndy+𝑵1sty𝑵2ndx2ndx𝑵2ndyV
8 6 7 fnmpoi +𝑝𝑸Fn𝑵×𝑵×𝑵×𝑵
9 elpqn A𝑸A𝑵×𝑵
10 elpqn B𝑸B𝑵×𝑵
11 opelxpi A𝑵×𝑵B𝑵×𝑵AB𝑵×𝑵×𝑵×𝑵
12 9 10 11 syl2an A𝑸B𝑸AB𝑵×𝑵×𝑵×𝑵
13 fvco2 +𝑝𝑸Fn𝑵×𝑵×𝑵×𝑵AB𝑵×𝑵×𝑵×𝑵/𝑸+𝑝𝑸AB=/𝑸+𝑝𝑸AB
14 8 12 13 sylancr A𝑸B𝑸/𝑸+𝑝𝑸AB=/𝑸+𝑝𝑸AB
15 3 5 14 3eqtrd A𝑸B𝑸+𝑸AB=/𝑸+𝑝𝑸AB
16 df-ov A+𝑸B=+𝑸AB
17 df-ov A+𝑝𝑸B=+𝑝𝑸AB
18 17 fveq2i /𝑸A+𝑝𝑸B=/𝑸+𝑝𝑸AB
19 15 16 18 3eqtr4g A𝑸B𝑸A+𝑸B=/𝑸A+𝑝𝑸B