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	⊢ +_pQ : ( ( N × N ) × ( N × N ) ) ⟶ ( N × N )

Proof

Step	Hyp	Ref	Expression
1		xp1st	⊢ ( 𝑥 ∈ ( N × N ) → ( 1^st ‘ 𝑥 ) ∈ N )
2		xp2nd	⊢ ( 𝑦 ∈ ( N × N ) → ( 2^nd ‘ 𝑦 ) ∈ N )
3		mulclpi	⊢ ( ( ( 1^st ‘ 𝑥 ) ∈ N ∧ ( 2^nd ‘ 𝑦 ) ∈ N ) → ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ∈ N )
4	1 2 3	syl2an	⊢ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) → ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ∈ N )
5		xp1st	⊢ ( 𝑦 ∈ ( N × N ) → ( 1^st ‘ 𝑦 ) ∈ N )
6		xp2nd	⊢ ( 𝑥 ∈ ( N × N ) → ( 2^nd ‘ 𝑥 ) ∈ N )
7		mulclpi	⊢ ( ( ( 1^st ‘ 𝑦 ) ∈ N ∧ ( 2^nd ‘ 𝑥 ) ∈ N ) → ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ∈ N )
8	5 6 7	syl2anr	⊢ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) → ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ∈ N )
9		addclpi	⊢ ( ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ∈ N ∧ ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ∈ N ) → ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) +_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) ∈ N )
10	4 8 9	syl2anc	⊢ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) → ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) +_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) ∈ N )
11		mulclpi	⊢ ( ( ( 2^nd ‘ 𝑥 ) ∈ N ∧ ( 2^nd ‘ 𝑦 ) ∈ N ) → ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ∈ N )
12	6 2 11	syl2an	⊢ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) → ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ∈ N )
13	10 12	opelxpd	⊢ ( ( 𝑥 ∈ ( N × N ) ∧ 𝑦 ∈ ( N × N ) ) → ⟨ ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) +_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) , ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ⟩ ∈ ( N × N ) )
14	13	rgen2	⊢ ∀ 𝑥 ∈ ( N × N ) ∀ 𝑦 ∈ ( N × N ) ⟨ ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) +_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) , ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ⟩ ∈ ( N × N )
15		df-plpq	⊢ +_pQ = ( 𝑥 ∈ ( N × N ) , 𝑦 ∈ ( N × N ) ↦ ⟨ ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) +_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) , ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ⟩ )
16	15	fmpo	⊢ ( ∀ 𝑥 ∈ ( N × N ) ∀ 𝑦 ∈ ( N × N ) ⟨ ( ( ( 1^st ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) +_N ( ( 1^st ‘ 𝑦 ) ·_N ( 2^nd ‘ 𝑥 ) ) ) , ( ( 2^nd ‘ 𝑥 ) ·_N ( 2^nd ‘ 𝑦 ) ) ⟩ ∈ ( N × N ) ↔ +_pQ : ( ( N × N ) × ( N × N ) ) ⟶ ( N × N ) )
17	14 16	mpbi	⊢ +_pQ : ( ( N × N ) × ( N × N ) ) ⟶ ( N × N )