Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  addcomnqg GIF version

 Description: Addition of positive fractions is commutative. (Contributed by Jim Kingdon, 15-Sep-2019.)
Assertion
Ref Expression
addcomnqg ((𝐴Q𝐵Q) → (𝐴 +Q 𝐵) = (𝐵 +Q 𝐴))

Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nqqs 7168 . 2 Q = ((N × N) / ~Q )
2 addpipqqs 7190 . 2 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → ([⟨𝑥, 𝑦⟩] ~Q +Q [⟨𝑧, 𝑤⟩] ~Q ) = [⟨((𝑥 ·N 𝑤) +N (𝑦 ·N 𝑧)), (𝑦 ·N 𝑤)⟩] ~Q )
3 addpipqqs 7190 . 2 (((𝑧N𝑤N) ∧ (𝑥N𝑦N)) → ([⟨𝑧, 𝑤⟩] ~Q +Q [⟨𝑥, 𝑦⟩] ~Q ) = [⟨((𝑧 ·N 𝑦) +N (𝑤 ·N 𝑥)), (𝑤 ·N 𝑦)⟩] ~Q )
4 mulcompig 7151 . . . . 5 ((𝑥N𝑤N) → (𝑥 ·N 𝑤) = (𝑤 ·N 𝑥))
5 mulcompig 7151 . . . . 5 ((𝑦N𝑧N) → (𝑦 ·N 𝑧) = (𝑧 ·N 𝑦))
64, 5oveqan12d 5793 . . . 4 (((𝑥N𝑤N) ∧ (𝑦N𝑧N)) → ((𝑥 ·N 𝑤) +N (𝑦 ·N 𝑧)) = ((𝑤 ·N 𝑥) +N (𝑧 ·N 𝑦)))
76an42s 578 . . 3 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → ((𝑥 ·N 𝑤) +N (𝑦 ·N 𝑧)) = ((𝑤 ·N 𝑥) +N (𝑧 ·N 𝑦)))
8 mulclpi 7148 . . . . . 6 ((𝑤N𝑥N) → (𝑤 ·N 𝑥) ∈ N)
98ancoms 266 . . . . 5 ((𝑥N𝑤N) → (𝑤 ·N 𝑥) ∈ N)
109ad2ant2rl 502 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → (𝑤 ·N 𝑥) ∈ N)
11 mulclpi 7148 . . . . . 6 ((𝑧N𝑦N) → (𝑧 ·N 𝑦) ∈ N)
1211ancoms 266 . . . . 5 ((𝑦N𝑧N) → (𝑧 ·N 𝑦) ∈ N)
1312ad2ant2lr 501 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → (𝑧 ·N 𝑦) ∈ N)
14 addcompig 7149 . . . 4 (((𝑤 ·N 𝑥) ∈ N ∧ (𝑧 ·N 𝑦) ∈ N) → ((𝑤 ·N 𝑥) +N (𝑧 ·N 𝑦)) = ((𝑧 ·N 𝑦) +N (𝑤 ·N 𝑥)))
1510, 13, 14syl2anc 408 . . 3 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → ((𝑤 ·N 𝑥) +N (𝑧 ·N 𝑦)) = ((𝑧 ·N 𝑦) +N (𝑤 ·N 𝑥)))
167, 15eqtrd 2172 . 2 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → ((𝑥 ·N 𝑤) +N (𝑦 ·N 𝑧)) = ((𝑧 ·N 𝑦) +N (𝑤 ·N 𝑥)))
17 mulcompig 7151 . . 3 ((𝑦N𝑤N) → (𝑦 ·N 𝑤) = (𝑤 ·N 𝑦))
1817ad2ant2l 499 . 2 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → (𝑦 ·N 𝑤) = (𝑤 ·N 𝑦))
191, 2, 3, 16, 18ecovicom 6537 1 ((𝐴Q𝐵Q) → (𝐴 +Q 𝐵) = (𝐵 +Q 𝐴))