Theorem addcompi

Description: Addition of positive integers is commutative. (Contributed by NM, 27-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	addcompi	$$⊢A{+}_{𝑵}B=B{+}_{𝑵}A$$

Proof

Step	Hyp	Ref	Expression
1		pinn	$$⊢A\in 𝑵\to A\in \mathrm{\omega }$$
2		pinn	$$⊢B\in 𝑵\to B\in \mathrm{\omega }$$
3		nnacom	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to A{+}_{𝑜}B=B{+}_{𝑜}A$$
4	1 2 3	syl2an	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to A{+}_{𝑜}B=B{+}_{𝑜}A$$
5		addpiord	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to A{+}_{𝑵}B=A{+}_{𝑜}B$$
6		addpiord	$$⊢\left(B\in 𝑵\wedge A\in 𝑵\right)\to B{+}_{𝑵}A=B{+}_{𝑜}A$$
7	6	ancoms	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to B{+}_{𝑵}A=B{+}_{𝑜}A$$
8	4 5 7	3eqtr4d	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to A{+}_{𝑵}B=B{+}_{𝑵}A$$
9		dmaddpi	$$⊢\mathrm{dom}{+}_{𝑵}=𝑵\times 𝑵$$
10	9	ndmovcom	$$⊢\neg \left(A\in 𝑵\wedge B\in 𝑵\right)\to A{+}_{𝑵}B=B{+}_{𝑵}A$$
11	8 10	pm2.61i	$$⊢A{+}_{𝑵}B=B{+}_{𝑵}A$$