Metamath Proof Explorer


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𝑵Aω
2 pinn B𝑵Bω
3 nnacom AωBωA+𝑜B=B+𝑜A
4 1 2 3 syl2an A𝑵B𝑵A+𝑜B=B+𝑜A
5 addpiord A𝑵B𝑵A+𝑵B=A+𝑜B
6 addpiord B𝑵A𝑵B+𝑵A=B+𝑜A
7 6 ancoms A𝑵B𝑵B+𝑵A=B+𝑜A
8 4 5 7 3eqtr4d A𝑵B𝑵A+𝑵B=B+𝑵A
9 dmaddpi dom+𝑵=𝑵×𝑵
10 9 ndmovcom ¬A𝑵B𝑵A+𝑵B=B+𝑵A
11 8 10 pm2.61i A+𝑵B=B+𝑵A