Metamath Proof Explorer

Theorem addpipq

Description: Addition of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	addpipq	$⊢ ((A \in 𝑵 \land B \in 𝑵) \land (C \in 𝑵 \land D \in 𝑵)) \to ⟨A, B⟩ +_{𝑝𝑸} ⟨C, D⟩ = ⟨(A \cdot_{𝑵} D) +_{𝑵} (C \cdot_{𝑵} B), 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		addpipq2	$⊢ (⟨A, B⟩ \in (𝑵 \times 𝑵) \land ⟨C, D⟩ \in (𝑵 \times 𝑵)) \to ⟨A, B⟩ +_{𝑝𝑸} ⟨C, D⟩ = ⟨(1^{st} (⟨A, B⟩) \cdot_{𝑵} 2^{nd} (⟨C, D⟩)) +_{𝑵} (1^{st} (⟨C, D⟩) \cdot_{𝑵} 2^{nd} (⟨A, B⟩)), 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⟩ +_{𝑝𝑸} ⟨C, D⟩ = ⟨(1^{st} (⟨A, B⟩) \cdot_{𝑵} 2^{nd} (⟨C, D⟩)) +_{𝑵} (1^{st} (⟨C, D⟩) \cdot_{𝑵} 2^{nd} (⟨A, B⟩)), 2^{nd} (⟨A, B⟩) \cdot_{𝑵} 2^{nd} (⟨C, D⟩)⟩$
5		op1stg	$⊢ (A \in 𝑵 \land B \in 𝑵) \to 1^{st} (⟨A, B⟩) = A$
6		op2ndg	$⊢ (C \in 𝑵 \land D \in 𝑵) \to 2^{nd} (⟨C, D⟩) = D$
7	5 6	oveqan12d	$⊢ ((A \in 𝑵 \land B \in 𝑵) \land (C \in 𝑵 \land D \in 𝑵)) \to 1^{st} (⟨A, B⟩) \cdot_{𝑵} 2^{nd} (⟨C, D⟩) = A \cdot_{𝑵} D$
8		op1stg	$⊢ (C \in 𝑵 \land D \in 𝑵) \to 1^{st} (⟨C, D⟩) = C$
9		op2ndg	$⊢ (A \in 𝑵 \land B \in 𝑵) \to 2^{nd} (⟨A, B⟩) = B$
10	8 9	oveqan12rd	$⊢ ((A \in 𝑵 \land B \in 𝑵) \land (C \in 𝑵 \land D \in 𝑵)) \to 1^{st} (⟨C, D⟩) \cdot_{𝑵} 2^{nd} (⟨A, B⟩) = C \cdot_{𝑵} B$
11	7 10	oveq12d	$⊢ ((A \in 𝑵 \land B \in 𝑵) \land (C \in 𝑵 \land D \in 𝑵)) \to (1^{st} (⟨A, B⟩) \cdot_{𝑵} 2^{nd} (⟨C, D⟩)) +_{𝑵} (1^{st} (⟨C, D⟩) \cdot_{𝑵} 2^{nd} (⟨A, B⟩)) = (A \cdot_{𝑵} D) +_{𝑵} (C \cdot_{𝑵} B)$
12	9 6	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$
13	11 12	opeq12d	$⊢ ((A \in 𝑵 \land B \in 𝑵) \land (C \in 𝑵 \land D \in 𝑵)) \to ⟨(1^{st} (⟨A, B⟩) \cdot_{𝑵} 2^{nd} (⟨C, D⟩)) +_{𝑵} (1^{st} (⟨C, D⟩) \cdot_{𝑵} 2^{nd} (⟨A, B⟩)), 2^{nd} (⟨A, B⟩) \cdot_{𝑵} 2^{nd} (⟨C, D⟩)⟩ = ⟨(A \cdot_{𝑵} D) +_{𝑵} (C \cdot_{𝑵} B), B \cdot_{𝑵} D⟩$
14	4 13	eqtrd	$⊢ ((A \in 𝑵 \land B \in 𝑵) \land (C \in 𝑵 \land D \in 𝑵)) \to ⟨A, B⟩ +_{𝑝𝑸} ⟨C, D⟩ = ⟨(A \cdot_{𝑵} D) +_{𝑵} (C \cdot_{𝑵} B), B \cdot_{𝑵} D⟩$