Metamath Proof Explorer


Theorem mulclnq

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 mulclnq A𝑸B𝑸A𝑸B𝑸

Proof

Step Hyp Ref Expression
1 mulpqnq A𝑸B𝑸A𝑸B=/𝑸A𝑝𝑸B
2 elpqn A𝑸A𝑵×𝑵
3 elpqn B𝑸B𝑵×𝑵
4 mulpqf 𝑝𝑸:𝑵×𝑵×𝑵×𝑵𝑵×𝑵
5 4 fovcl A𝑵×𝑵B𝑵×𝑵A𝑝𝑸B𝑵×𝑵
6 2 3 5 syl2an A𝑸B𝑸A𝑝𝑸B𝑵×𝑵
7 nqercl A𝑝𝑸B𝑵×𝑵/𝑸A𝑝𝑸B𝑸
8 6 7 syl A𝑸B𝑸/𝑸A𝑝𝑸B𝑸
9 1 8 eqeltrd A𝑸B𝑸A𝑸B𝑸