Metamath Proof Explorer

Theorem mulpipq

Description: Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	mulpipq	$⊢ ((A \in 𝑵 \land B \in 𝑵) \land (C \in 𝑵 \land D \in 𝑵)) \to ⟨A, B⟩ \cdot_{𝑝𝑸} ⟨C, D⟩ = ⟨A \cdot_{𝑵} C, B \cdot_{𝑵} D⟩$

Proof

Step	Hyp	Ref	Expression
1		opelxpi	$⊢ (A \in 𝑵 \land B \in 𝑵) \to ⟨A, B⟩ \in (𝑵 \times 𝑵)$
2		opelxpi	$⊢ (C \in 𝑵 \land D \in 𝑵) \to ⟨C, D⟩ \in (𝑵 \times 𝑵)$
3		mulpipq2	$⊢ (⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵)) \to ⟨A, B⟩ \cdot_{𝑝𝑸} ⟨C, D⟩ = ⟨1^{st} (⟨A, B⟩) \cdot_{𝑵} 1^{st} (⟨C, D⟩), 2^{nd} (⟨A, B⟩) \cdot_{𝑵} 2^{nd} (⟨C, D⟩)⟩$
4	1 2 3	syl2an	$⊢ ((A \in 𝑵 \land B \in 𝑵) \land (C \in 𝑵 \land D \in 𝑵)) \to ⟨A, B⟩ \cdot_{𝑝𝑸} ⟨C, D⟩ = ⟨1^{st} (⟨A, B⟩) \cdot_{𝑵} 1^{st} (⟨C, D⟩), 2^{nd} (⟨A, B⟩) \cdot_{𝑵} 2^{nd} (⟨C, D⟩)⟩$
5		op1stg	$⊢ (A \in 𝑵 \land B \in 𝑵) \to 1^{st} (⟨A, B⟩) = A$
6		op1stg	$⊢ (C \in 𝑵 \land D \in 𝑵) \to 1^{st} (⟨C, D⟩) = C$
7	5 6	oveqan12d	$⊢ ((A \in 𝑵 \land B \in 𝑵) \land (C \in 𝑵 \land D \in 𝑵)) \to 1^{st} (⟨A, B⟩) \cdot_{𝑵} 1^{st} (⟨C, D⟩) = A \cdot_{𝑵} C$
8		op2ndg	$⊢ (A \in 𝑵 \land B \in 𝑵) \to 2^{nd} (⟨A, B⟩) = B$
9		op2ndg	$⊢ (C \in 𝑵 \land D \in 𝑵) \to 2^{nd} (⟨C, D⟩) = D$
10	8 9	oveqan12d	$⊢ ((A \in 𝑵 \land B \in 𝑵) \land (C \in 𝑵 \land D \in 𝑵)) \to 2^{nd} (⟨A, B⟩) \cdot_{𝑵} 2^{nd} (⟨C, D⟩) = B \cdot_{𝑵} D$
11	7 10	opeq12d	$⊢ ((A \in 𝑵 \land B \in 𝑵) \land (C \in 𝑵 \land D \in 𝑵)) \to ⟨1^{st} (⟨A, B⟩) \cdot_{𝑵} 1^{st} (⟨C, D⟩), 2^{nd} (⟨A, B⟩) \cdot_{𝑵} 2^{nd} (⟨C, D⟩)⟩ = ⟨A \cdot_{𝑵} C, B \cdot_{𝑵} D⟩$
12	4 11	eqtrd	$⊢ ((A \in 𝑵 \land B \in 𝑵) \land (C \in 𝑵 \land D \in 𝑵)) \to ⟨A, B⟩ \cdot_{𝑝𝑸} ⟨C, D⟩ = ⟨A \cdot_{𝑵} C, B \cdot_{𝑵} D⟩$