Metamath Proof Explorer


Theorem mulpqnq

Description: Multiplication 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 mulpqnq A 𝑸 B 𝑸 A 𝑸 B = / 𝑸 A 𝑝𝑸 B

Proof

Step Hyp Ref Expression
1 df-mq 𝑸 = / 𝑸 𝑝𝑸 𝑸 × 𝑸
2 1 fveq1i 𝑸 A B = / 𝑸 𝑝𝑸 𝑸 × 𝑸 A B
3 2 a1i A 𝑸 B 𝑸 𝑸 A B = / 𝑸 𝑝𝑸 𝑸 × 𝑸 A B
4 opelxpi A 𝑸 B 𝑸 A B 𝑸 × 𝑸
5 4 fvresd A 𝑸 B 𝑸 / 𝑸 𝑝𝑸 𝑸 × 𝑸 A B = / 𝑸 𝑝𝑸 A B
6 df-mpq 𝑝𝑸 = x 𝑵 × 𝑵 , y 𝑵 × 𝑵 1 st x 𝑵 1 st y 2 nd x 𝑵 2 nd y
7 opex 1 st x 𝑵 1 st y 2 nd x 𝑵 2 nd y V
8 6 7 fnmpoi 𝑝𝑸 Fn 𝑵 × 𝑵 × 𝑵 × 𝑵
9 elpqn A 𝑸 A 𝑵 × 𝑵
10 elpqn B 𝑸 B 𝑵 × 𝑵
11 opelxpi A 𝑵 × 𝑵 B 𝑵 × 𝑵 A B 𝑵 × 𝑵 × 𝑵 × 𝑵
12 9 10 11 syl2an A 𝑸 B 𝑸 A B 𝑵 × 𝑵 × 𝑵 × 𝑵
13 fvco2 𝑝𝑸 Fn 𝑵 × 𝑵 × 𝑵 × 𝑵 A B 𝑵 × 𝑵 × 𝑵 × 𝑵 / 𝑸 𝑝𝑸 A B = / 𝑸 𝑝𝑸 A B
14 8 12 13 sylancr A 𝑸 B 𝑸 / 𝑸 𝑝𝑸 A B = / 𝑸 𝑝𝑸 A B
15 3 5 14 3eqtrd A 𝑸 B 𝑸 𝑸 A B = / 𝑸 𝑝𝑸 A B
16 df-ov A 𝑸 B = 𝑸 A B
17 df-ov A 𝑝𝑸 B = 𝑝𝑸 A B
18 17 fveq2i / 𝑸 A 𝑝𝑸 B = / 𝑸 𝑝𝑸 A B
19 15 16 18 3eqtr4g A 𝑸 B 𝑸 A 𝑸 B = / 𝑸 A 𝑝𝑸 B