Theorem mulcompi

Description: Multiplication of positive integers is commutative. (Contributed by NM, 21-Sep-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	mulcompi	$$⊢A{\cdot }_{𝑵}B=B{\cdot }_{𝑵}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		nnmcom	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to A{\cdot }_{𝑜}B=B{\cdot }_{𝑜}A$$
4	1 2 3	syl2an	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to A{\cdot }_{𝑜}B=B{\cdot }_{𝑜}A$$
5		mulpiord	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to A{\cdot }_{𝑵}B=A{\cdot }_{𝑜}B$$
6		mulpiord	$$⊢\left(B\in 𝑵\wedge A\in 𝑵\right)\to B{\cdot }_{𝑵}A=B{\cdot }_{𝑜}A$$
7	6	ancoms	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to B{\cdot }_{𝑵}A=B{\cdot }_{𝑜}A$$
8	4 5 7	3eqtr4d	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to A{\cdot }_{𝑵}B=B{\cdot }_{𝑵}A$$
9		dmmulpi	$$⊢\mathrm{dom}{\cdot }_{𝑵}=𝑵\times 𝑵$$
10	9	ndmovcom	$$⊢\neg \left(A\in 𝑵\wedge B\in 𝑵\right)\to A{\cdot }_{𝑵}B=B{\cdot }_{𝑵}A$$
11	8 10	pm2.61i	$$⊢A{\cdot }_{𝑵}B=B{\cdot }_{𝑵}A$$