Metamath Proof Explorer

Theorem mulcompi

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

Ref Expression
Assertion mulcompi ⊢ A ⋅ 𝑵 B = B ⋅ 𝑵 A

Proof

Step Hyp Ref Expression
1 pinn ⊢ A ∈ 𝑵 → A ∈ ω
2 pinn ⊢ B ∈ 𝑵 → B ∈ ω
3 nnmcom ⊢ A ∈ ω ∧ B ∈ ω → A ⋅ 𝑜 B = B ⋅ 𝑜 A
4 1 2 3 syl2an ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑜 B = B ⋅ 𝑜 A
5 mulpiord ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑵 B = A ⋅ 𝑜 B
6 mulpiord ⊢ 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 dmmulpi ⊢ dom ⁡ ⋅ 𝑵 = 𝑵 × 𝑵
10 9 ndmovcom ⊢ ¬ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ⋅ 𝑵 B = B ⋅ 𝑵 A
11 8 10 pm2.61i ⊢ A ⋅ 𝑵 B = B ⋅ 𝑵 A