Metamath Proof Explorer

Theorem nnmcom

Description: Multiplication of natural numbers is commutative. Theorem 4K(5) of Enderton p. 81. (Contributed by NM, 21-Sep-1995) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion nnmcom ⊢ A ∈ ω ∧ B ∈ ω → A ⋅ 𝑜 B = B ⋅ 𝑜 A

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ x = A → x ⋅ 𝑜 B = A ⋅ 𝑜 B
2 oveq2 ⊢ x = A → B ⋅ 𝑜 x = B ⋅ 𝑜 A
3 1 2 eqeq12d ⊢ x = A → x ⋅ 𝑜 B = B ⋅ 𝑜 x ↔ A ⋅ 𝑜 B = B ⋅ 𝑜 A
4 3 imbi2d ⊢ x = A → B ∈ ω → x ⋅ 𝑜 B = B ⋅ 𝑜 x ↔ B ∈ ω → A ⋅ 𝑜 B = B ⋅ 𝑜 A
5 oveq1 ⊢ x = ∅ → x ⋅ 𝑜 B = ∅ ⋅ 𝑜 B
6 oveq2 ⊢ x = ∅ → B ⋅ 𝑜 x = B ⋅ 𝑜 ∅
7 5 6 eqeq12d ⊢ x = ∅ → x ⋅ 𝑜 B = B ⋅ 𝑜 x ↔ ∅ ⋅ 𝑜 B = B ⋅ 𝑜 ∅
8 oveq1 ⊢ x = y → x ⋅ 𝑜 B = y ⋅ 𝑜 B
9 oveq2 ⊢ x = y → B ⋅ 𝑜 x = B ⋅ 𝑜 y
10 8 9 eqeq12d ⊢ x = y → x ⋅ 𝑜 B = B ⋅ 𝑜 x ↔ y ⋅ 𝑜 B = B ⋅ 𝑜 y
11 oveq1 ⊢ x = suc ⁡ y → x ⋅ 𝑜 B = suc ⁡ y ⋅ 𝑜 B
12 oveq2 ⊢ x = suc ⁡ y → B ⋅ 𝑜 x = B ⋅ 𝑜 suc ⁡ y
13 11 12 eqeq12d ⊢ x = suc ⁡ y → x ⋅ 𝑜 B = B ⋅ 𝑜 x ↔ suc ⁡ y ⋅ 𝑜 B = B ⋅ 𝑜 suc ⁡ y
14 nnm0r ⊢ B ∈ ω → ∅ ⋅ 𝑜 B = ∅
15 nnm0 ⊢ B ∈ ω → B ⋅ 𝑜 ∅ = ∅
16 14 15 eqtr4d ⊢ B ∈ ω → ∅ ⋅ 𝑜 B = B ⋅ 𝑜 ∅
17 oveq1 ⊢ y ⋅ 𝑜 B = B ⋅ 𝑜 y → y ⋅ 𝑜 B + 𝑜 B = B ⋅ 𝑜 y + 𝑜 B
18 nnmsucr ⊢ y ∈ ω ∧ B ∈ ω → suc ⁡ y ⋅ 𝑜 B = y ⋅ 𝑜 B + 𝑜 B
19 nnmsuc ⊢ B ∈ ω ∧ y ∈ ω → B ⋅ 𝑜 suc ⁡ y = B ⋅ 𝑜 y + 𝑜 B
20 19 ancoms ⊢ y ∈ ω ∧ B ∈ ω → B ⋅ 𝑜 suc ⁡ y = B ⋅ 𝑜 y + 𝑜 B
21 18 20 eqeq12d ⊢ y ∈ ω ∧ B ∈ ω → suc ⁡ y ⋅ 𝑜 B = B ⋅ 𝑜 suc ⁡ y ↔ y ⋅ 𝑜 B + 𝑜 B = B ⋅ 𝑜 y + 𝑜 B
22 17 21 syl5ibr ⊢ y ∈ ω ∧ B ∈ ω → y ⋅ 𝑜 B = B ⋅ 𝑜 y → suc ⁡ y ⋅ 𝑜 B = B ⋅ 𝑜 suc ⁡ y
23 22 ex ⊢ y ∈ ω → B ∈ ω → y ⋅ 𝑜 B = B ⋅ 𝑜 y → suc ⁡ y ⋅ 𝑜 B = B ⋅ 𝑜 suc ⁡ y
24 7 10 13 16 23 finds2 ⊢ x ∈ ω → B ∈ ω → x ⋅ 𝑜 B = B ⋅ 𝑜 x
25 4 24 vtoclga ⊢ A ∈ ω → B ∈ ω → A ⋅ 𝑜 B = B ⋅ 𝑜 A
26 25 imp ⊢ A ∈ ω ∧ B ∈ ω → A ⋅ 𝑜 B = B ⋅ 𝑜 A