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$

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

Metamath Proof Explorer