This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem addcomnq

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 addcomnq ⊢ A + 𝑸 B = B + 𝑸 A

Proof

Step Hyp Ref Expression
1 addcompq ⊢ A + 𝑝𝑸 B = B + 𝑝𝑸 A
2 1 fveq2i ⊢ / 𝑸 ⁡ A + 𝑝𝑸 B = / 𝑸 ⁡ B + 𝑝𝑸 A
3 addpqnq ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → A + 𝑸 B = / 𝑸 ⁡ A + 𝑝𝑸 B
4 addpqnq ⊢ B ∈ 𝑸 ∧ A ∈ 𝑸 → B + 𝑸 A = / 𝑸 ⁡ B + 𝑝𝑸 A
5 4 ancoms ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → B + 𝑸 A = / 𝑸 ⁡ B + 𝑝𝑸 A
6 2 3 5 3eqtr4a ⊢ A ∈ 𝑸 ∧ B ∈ 𝑸 → A + 𝑸 B = B + 𝑸 A
7 addnqf ⊢ + 𝑸 : 𝑸 × 𝑸 ⟶ 𝑸
8 7 fdmi ⊢ dom ⁡ + 𝑸 = 𝑸 × 𝑸
9 8 ndmovcom ⊢ ¬ A ∈ 𝑸 ∧ B ∈ 𝑸 → A + 𝑸 B = B + 𝑸 A
10 6 9 pm2.61i ⊢ A + 𝑸 B = B + 𝑸 A