Metamath Proof Explorer

Theorem addpqf

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	addpqf	$⊢ +_{𝑝𝑸} : (𝑵 \times 𝑵) \times (𝑵 \times 𝑵) ⟶ 𝑵 \times 𝑵$

Proof

Step	Hyp	Ref	Expression
1		xp1st	$⊢ x \in (𝑵 \times 𝑵) \to 1^{st} (x) \in 𝑵$
2		xp2nd	$⊢ y \in (𝑵 \times 𝑵) \to 2^{nd} (y) \in 𝑵$
3		mulclpi	$⊢ (1^{st} (x) \in 𝑵 \land 2^{nd} (y) \in 𝑵) \to 1^{st} (x) \cdot_{𝑵} 2^{nd} (y) \in 𝑵$
4	1 2 3	syl2an	$⊢ (x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \to 1^{st} (x) \cdot_{𝑵} 2^{nd} (y) \in 𝑵$
5		xp1st	$⊢ y \in (𝑵 \times 𝑵) \to 1^{st} (y) \in 𝑵$
6		xp2nd	$⊢ x \in (𝑵 \times 𝑵) \to 2^{nd} (x) \in 𝑵$
7		mulclpi	$⊢ (1^{st} (y) \in 𝑵 \land 2^{nd} (x) \in 𝑵) \to 1^{st} (y) \cdot_{𝑵} 2^{nd} (x) \in 𝑵$
8	5 6 7	syl2anr	$⊢ (x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \to 1^{st} (y) \cdot_{𝑵} 2^{nd} (x) \in 𝑵$
9		addclpi	$⊢ (1^{st} (x) \cdot_{𝑵} 2^{nd} (y) \in 𝑵 \land 1^{st} (y) \cdot_{𝑵} 2^{nd} (x) \in 𝑵) \to (1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) +_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)) \in 𝑵$
10	4 8 9	syl2anc	$⊢ (x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \to (1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) +_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)) \in 𝑵$
11		mulclpi	$⊢ (2^{nd} (x) \in 𝑵 \land 2^{nd} (y) \in 𝑵) \to 2^{nd} (x) \cdot_{𝑵} 2^{nd} (y) \in 𝑵$
12	6 2 11	syl2an	$⊢ (x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \to 2^{nd} (x) \cdot_{𝑵} 2^{nd} (y) \in 𝑵$
13	10 12	opelxpd	$⊢ (x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \to ⟨(1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) +_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)), 2^{nd} (x) \cdot_{𝑵} 2^{nd} (y)⟩ \in (𝑵 \times 𝑵)$
14	13	rgen2	$⊢ \forall x \in (𝑵 \times 𝑵) \forall y \in (𝑵 \times 𝑵) ⟨(1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) +_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)), 2^{nd} (x) \cdot_{𝑵} 2^{nd} (y)⟩ \in (𝑵 \times 𝑵)$
15		df-plpq	$⊢ +_{𝑝𝑸} = (x \in (𝑵 \times 𝑵), y \in (𝑵 \times 𝑵) ⟼ ⟨(1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) +_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)), 2^{nd} (x) \cdot_{𝑵} 2^{nd} (y)⟩)$
16	15	fmpo	$⊢ \forall x \in (𝑵 \times 𝑵) \forall y \in (𝑵 \times 𝑵) ⟨(1^{st} (x) \cdot_{𝑵} 2^{nd} (y)) +_{𝑵} (1^{st} (y) \cdot_{𝑵} 2^{nd} (x)), 2^{nd} (x) \cdot_{𝑵} 2^{nd} (y)⟩ \in (𝑵 \times 𝑵) \leftrightarrow +_{𝑝𝑸} : (𝑵 \times 𝑵) \times (𝑵 \times 𝑵) ⟶ 𝑵 \times 𝑵$
17	14 16	mpbi	$⊢ +_{𝑝𝑸} : (𝑵 \times 𝑵) \times (𝑵 \times 𝑵) ⟶ 𝑵 \times 𝑵$