Metamath Proof Explorer


Theorem mulpqf

Description: Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

Ref Expression
Assertion mulpqf 𝑝𝑸 : 𝑵 × 𝑵 × 𝑵 × 𝑵 𝑵 × 𝑵

Proof

Step Hyp Ref Expression
1 xp1st x 𝑵 × 𝑵 1 st x 𝑵
2 xp1st y 𝑵 × 𝑵 1 st y 𝑵
3 mulclpi 1 st x 𝑵 1 st y 𝑵 1 st x 𝑵 1 st y 𝑵
4 1 2 3 syl2an x 𝑵 × 𝑵 y 𝑵 × 𝑵 1 st x 𝑵 1 st y 𝑵
5 xp2nd x 𝑵 × 𝑵 2 nd x 𝑵
6 xp2nd y 𝑵 × 𝑵 2 nd y 𝑵
7 mulclpi 2 nd x 𝑵 2 nd y 𝑵 2 nd x 𝑵 2 nd y 𝑵
8 5 6 7 syl2an x 𝑵 × 𝑵 y 𝑵 × 𝑵 2 nd x 𝑵 2 nd y 𝑵
9 4 8 opelxpd x 𝑵 × 𝑵 y 𝑵 × 𝑵 1 st x 𝑵 1 st y 2 nd x 𝑵 2 nd y 𝑵 × 𝑵
10 9 rgen2 x 𝑵 × 𝑵 y 𝑵 × 𝑵 1 st x 𝑵 1 st y 2 nd x 𝑵 2 nd y 𝑵 × 𝑵
11 df-mpq 𝑝𝑸 = x 𝑵 × 𝑵 , y 𝑵 × 𝑵 1 st x 𝑵 1 st y 2 nd x 𝑵 2 nd y
12 11 fmpo x 𝑵 × 𝑵 y 𝑵 × 𝑵 1 st x 𝑵 1 st y 2 nd x 𝑵 2 nd y 𝑵 × 𝑵 𝑝𝑸 : 𝑵 × 𝑵 × 𝑵 × 𝑵 𝑵 × 𝑵
13 10 12 mpbi 𝑝𝑸 : 𝑵 × 𝑵 × 𝑵 × 𝑵 𝑵 × 𝑵