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 \in 𝑸 \land B \in 𝑸) \to A \cdot_{𝑸} B \in 𝑸$

Proof

Step	Hyp	Ref	Expression
1		mulpqnq	$⊢ (A \in 𝑸 \land B \in 𝑸) \to A \cdot_{𝑸} B = /_{𝑸} (A \cdot_{𝑝𝑸} B)$
2		elpqn	$⊢ A \in 𝑸 \to A \in (𝑵 \times 𝑵)$
3		elpqn	$⊢ B \in 𝑸 \to B \in (𝑵 \times 𝑵)$
4		mulpqf	$⊢ \cdot_{𝑝𝑸} : (𝑵 \times 𝑵) \times (𝑵 \times 𝑵) ⟶ 𝑵 \times 𝑵$
5	4	fovcl	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to A \cdot_{𝑝𝑸} B \in (𝑵 \times 𝑵)$
6	2 3 5	syl2an	$⊢ (A \in 𝑸 \land B \in 𝑸) \to A \cdot_{𝑝𝑸} B \in (𝑵 \times 𝑵)$
7		nqercl	$⊢ A \cdot_{𝑝𝑸} B \in (𝑵 \times 𝑵) \to /_{𝑸} (A \cdot_{𝑝𝑸} B) \in 𝑸$
8	6 7	syl	$⊢ (A \in 𝑸 \land B \in 𝑸) \to /_{𝑸} (A \cdot_{𝑝𝑸} B) \in 𝑸$
9	1 8	eqeltrd	$⊢ (A \in 𝑸 \land B \in 𝑸) \to A \cdot_{𝑸} B \in 𝑸$