Metamath Proof Explorer

Theorem addcompq

Description: Addition of positive fractions is commutative. (Contributed by NM, 30-Aug-1995) (Revised by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	addcompq	$⊢ A +_{𝑝𝑸} B = B +_{𝑝𝑸} A$

Proof

Step	Hyp	Ref	Expression
1		addcompi	$⊢ (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) = (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B))$
2		mulcompi	$⊢ 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B) = 2^{nd} (B) \cdot_{𝑵} 2^{nd} (A)$
3	1 2	opeq12i	$⊢ ⟨(1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩ = ⟨(1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (A)⟩$
4		addpipq2	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to A +_{𝑝𝑸} B = ⟨(1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩$
5		addpipq2	$⊢ (B \in (𝑵 \times 𝑵) \land A \in (𝑵 \times 𝑵)) \to B +_{𝑝𝑸} A = ⟨(1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (A)⟩$
6	5	ancoms	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to B +_{𝑝𝑸} A = ⟨(1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) +_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)), 2^{nd} (B) \cdot_{𝑵} 2^{nd} (A)⟩$
7	3 4 6	3eqtr4a	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to A +_{𝑝𝑸} B = B +_{𝑝𝑸} A$
8		addpqf	$⊢ +_{𝑝𝑸} : (𝑵 \times 𝑵) \times (𝑵 \times 𝑵) ⟶ 𝑵 \times 𝑵$
9	8	fdmi	$⊢ dom +_{𝑝𝑸} = (𝑵 \times 𝑵) \times (𝑵 \times 𝑵)$
10	9	ndmovcom	$⊢ \neg (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to A +_{𝑝𝑸} B = B +_{𝑝𝑸} A$
11	7 10	pm2.61i	$⊢ A +_{𝑝𝑸} B = B +_{𝑝𝑸} A$