This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem addclnq

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

		Ref	Expression
	Assertion	addclnq	$⊢ (A \in 𝑸 \land B \in 𝑸) \to A +_{𝑸} B \in 𝑸$

Proof

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