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 ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o 𝐵 ) = ( 𝐵 ·o 𝐴 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ·o 𝐵 ) = ( 𝐴 ·o 𝐵 ) )
2 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐵 ·o 𝑥 ) = ( 𝐵 ·o 𝐴 ) )
3 1 2 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ·o 𝐵 ) = ( 𝐵 ·o 𝑥 ) ↔ ( 𝐴 ·o 𝐵 ) = ( 𝐵 ·o 𝐴 ) ) )
4 3 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐵 ∈ ω → ( 𝑥 ·o 𝐵 ) = ( 𝐵 ·o 𝑥 ) ) ↔ ( 𝐵 ∈ ω → ( 𝐴 ·o 𝐵 ) = ( 𝐵 ·o 𝐴 ) ) ) )
5 oveq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ·o 𝐵 ) = ( ∅ ·o 𝐵 ) )
6 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐵 ·o 𝑥 ) = ( 𝐵 ·o ∅ ) )
7 5 6 eqeq12d ⊢ ( 𝑥 = ∅ → ( ( 𝑥 ·o 𝐵 ) = ( 𝐵 ·o 𝑥 ) ↔ ( ∅ ·o 𝐵 ) = ( 𝐵 ·o ∅ ) ) )
8 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ·o 𝐵 ) = ( 𝑦 ·o 𝐵 ) )
9 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ·o 𝑥 ) = ( 𝐵 ·o 𝑦 ) )
10 8 9 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ·o 𝐵 ) = ( 𝐵 ·o 𝑥 ) ↔ ( 𝑦 ·o 𝐵 ) = ( 𝐵 ·o 𝑦 ) ) )
11 oveq1 ⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 ·o 𝐵 ) = ( suc 𝑦 ·o 𝐵 ) )
12 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐵 ·o 𝑥 ) = ( 𝐵 ·o suc 𝑦 ) )
13 11 12 eqeq12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑥 ·o 𝐵 ) = ( 𝐵 ·o 𝑥 ) ↔ ( suc 𝑦 ·o 𝐵 ) = ( 𝐵 ·o suc 𝑦 ) ) )
14 nnm0r ⊢ ( 𝐵 ∈ ω → ( ∅ ·o 𝐵 ) = ∅ )
15 nnm0 ⊢ ( 𝐵 ∈ ω → ( 𝐵 ·o ∅ ) = ∅ )
16 14 15 eqtr4d ⊢ ( 𝐵 ∈ ω → ( ∅ ·o 𝐵 ) = ( 𝐵 ·o ∅ ) )
17 oveq1 ⊢ ( ( 𝑦 ·o 𝐵 ) = ( 𝐵 ·o 𝑦 ) → ( ( 𝑦 ·o 𝐵 ) +o 𝐵 ) = ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) )
18 nnmsucr ⊢ ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) → ( suc 𝑦 ·o 𝐵 ) = ( ( 𝑦 ·o 𝐵 ) +o 𝐵 ) )
19 nnmsuc ⊢ ( ( 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐵 ·o suc 𝑦 ) = ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) )
20 19 ancoms ⊢ ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵 ·o suc 𝑦 ) = ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) )
21 18 20 eqeq12d ⊢ ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( suc 𝑦 ·o 𝐵 ) = ( 𝐵 ·o suc 𝑦 ) ↔ ( ( 𝑦 ·o 𝐵 ) +o 𝐵 ) = ( ( 𝐵 ·o 𝑦 ) +o 𝐵 ) ) )
22 17 21 syl5ibr ⊢ ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝑦 ·o 𝐵 ) = ( 𝐵 ·o 𝑦 ) → ( suc 𝑦 ·o 𝐵 ) = ( 𝐵 ·o suc 𝑦 ) ) )
23 22 ex ⊢ ( 𝑦 ∈ ω → ( 𝐵 ∈ ω → ( ( 𝑦 ·o 𝐵 ) = ( 𝐵 ·o 𝑦 ) → ( suc 𝑦 ·o 𝐵 ) = ( 𝐵 ·o suc 𝑦 ) ) ) )
24 7 10 13 16 23 finds2 ⊢ ( 𝑥 ∈ ω → ( 𝐵 ∈ ω → ( 𝑥 ·o 𝐵 ) = ( 𝐵 ·o 𝑥 ) ) )
25 4 24 vtoclga ⊢ ( 𝐴 ∈ ω → ( 𝐵 ∈ ω → ( 𝐴 ·o 𝐵 ) = ( 𝐵 ·o 𝐴 ) ) )
26 25 imp ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o 𝐵 ) = ( 𝐵 ·o 𝐴 ) )