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{+}_{\mathrm{𝑝𝑸}}B=B{+}_{\mathrm{𝑝𝑸}}A$$

Proof

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