Metamath Proof Explorer

Theorem nnmass

Description: Multiplication of natural numbers is associative. Theorem 4K(4) of Enderton p. 81. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 15-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ x = C → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 C
2 oveq2 ⊢ x = C → B ⋅ 𝑜 x = B ⋅ 𝑜 C
3 2 oveq2d ⊢ x = C → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 C
4 1 3 eqeq12d ⊢ x = C → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 x ↔ A ⋅ 𝑜 B ⋅ 𝑜 C = A ⋅ 𝑜 B ⋅ 𝑜 C
5 4 imbi2d ⊢ x = C → A ∈ ω ∧ B ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 x ↔ A ∈ ω ∧ B ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 C = A ⋅ 𝑜 B ⋅ 𝑜 C
6 oveq2 ⊢ x = ∅ → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 ∅
7 oveq2 ⊢ x = ∅ → B ⋅ 𝑜 x = B ⋅ 𝑜 ∅
8 7 oveq2d ⊢ x = ∅ → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 ∅
9 6 8 eqeq12d ⊢ x = ∅ → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 x ↔ A ⋅ 𝑜 B ⋅ 𝑜 ∅ = A ⋅ 𝑜 B ⋅ 𝑜 ∅
10 oveq2 ⊢ x = y → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 y
11 oveq2 ⊢ x = y → B ⋅ 𝑜 x = B ⋅ 𝑜 y
12 11 oveq2d ⊢ x = y → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 y
13 10 12 eqeq12d ⊢ x = y → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 x ↔ A ⋅ 𝑜 B ⋅ 𝑜 y = A ⋅ 𝑜 B ⋅ 𝑜 y
14 oveq2 ⊢ x = suc ⁡ y → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y
15 oveq2 ⊢ x = suc ⁡ y → B ⋅ 𝑜 x = B ⋅ 𝑜 suc ⁡ y
16 15 oveq2d ⊢ x = suc ⁡ y → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y
17 14 16 eqeq12d ⊢ x = suc ⁡ y → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 x ↔ A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y
18 nnmcl ⊢ A ∈ ω ∧ B ∈ ω → A ⋅ 𝑜 B ∈ ω
19 nnm0 ⊢ A ⋅ 𝑜 B ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 ∅ = ∅
20 18 19 syl ⊢ A ∈ ω ∧ B ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 ∅ = ∅
21 nnm0 ⊢ B ∈ ω → B ⋅ 𝑜 ∅ = ∅
22 21 oveq2d ⊢ B ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 ∅ = A ⋅ 𝑜 ∅
23 nnm0 ⊢ A ∈ ω → A ⋅ 𝑜 ∅ = ∅
24 22 23 sylan9eqr ⊢ A ∈ ω ∧ B ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 ∅ = ∅
25 20 24 eqtr4d ⊢ A ∈ ω ∧ B ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 ∅ = A ⋅ 𝑜 B ⋅ 𝑜 ∅
26 oveq1 ⊢ A ⋅ 𝑜 B ⋅ 𝑜 y = A ⋅ 𝑜 B ⋅ 𝑜 y → A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 A ⋅ 𝑜 B = A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 A ⋅ 𝑜 B
27 nnmsuc ⊢ A ⋅ 𝑜 B ∈ ω ∧ y ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 A ⋅ 𝑜 B
28 18 27 stoic3 ⊢ A ∈ ω ∧ B ∈ ω ∧ y ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 A ⋅ 𝑜 B
29 nnmsuc ⊢ B ∈ ω ∧ y ∈ ω → B ⋅ 𝑜 suc ⁡ y = B ⋅ 𝑜 y + 𝑜 B
30 29 3adant1 ⊢ A ∈ ω ∧ B ∈ ω ∧ y ∈ ω → B ⋅ 𝑜 suc ⁡ y = B ⋅ 𝑜 y + 𝑜 B
31 30 oveq2d ⊢ A ∈ ω ∧ B ∈ ω ∧ y ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 B
32 nnmcl ⊢ B ∈ ω ∧ y ∈ ω → B ⋅ 𝑜 y ∈ ω
33 nndi ⊢ A ∈ ω ∧ B ⋅ 𝑜 y ∈ ω ∧ B ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 B = A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 A ⋅ 𝑜 B
34 32 33 syl3an2 ⊢ A ∈ ω ∧ B ∈ ω ∧ y ∈ ω ∧ B ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 B = A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 A ⋅ 𝑜 B
35 34 3exp ⊢ A ∈ ω → B ∈ ω ∧ y ∈ ω → B ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 B = A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 A ⋅ 𝑜 B
36 35 expd ⊢ A ∈ ω → B ∈ ω → y ∈ ω → B ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 B = A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 A ⋅ 𝑜 B
37 36 com34 ⊢ A ∈ ω → B ∈ ω → B ∈ ω → y ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 B = A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 A ⋅ 𝑜 B
38 37 pm2.43d ⊢ A ∈ ω → B ∈ ω → y ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 B = A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 A ⋅ 𝑜 B
39 38 3imp ⊢ A ∈ ω ∧ B ∈ ω ∧ y ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 B = A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 A ⋅ 𝑜 B
40 31 39 eqtrd ⊢ A ∈ ω ∧ B ∈ ω ∧ y ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 A ⋅ 𝑜 B
41 28 40 eqeq12d ⊢ A ∈ ω ∧ B ∈ ω ∧ y ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y ↔ A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 A ⋅ 𝑜 B = A ⋅ 𝑜 B ⋅ 𝑜 y + 𝑜 A ⋅ 𝑜 B
42 26 41 syl5ibr ⊢ A ∈ ω ∧ B ∈ ω ∧ y ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 y = A ⋅ 𝑜 B ⋅ 𝑜 y → A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y
43 42 3exp ⊢ A ∈ ω → B ∈ ω → y ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 y = A ⋅ 𝑜 B ⋅ 𝑜 y → A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y
44 43 com3r ⊢ y ∈ ω → A ∈ ω → B ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 y = A ⋅ 𝑜 B ⋅ 𝑜 y → A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y
45 44 impd ⊢ y ∈ ω → A ∈ ω ∧ B ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 y = A ⋅ 𝑜 B ⋅ 𝑜 y → A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y = A ⋅ 𝑜 B ⋅ 𝑜 suc ⁡ y
46 9 13 17 25 45 finds2 ⊢ x ∈ ω → A ∈ ω ∧ B ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 x = A ⋅ 𝑜 B ⋅ 𝑜 x
47 5 46 vtoclga ⊢ C ∈ ω → A ∈ ω ∧ B ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 C = A ⋅ 𝑜 B ⋅ 𝑜 C
48 47 expdcom ⊢ A ∈ ω → B ∈ ω → C ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 C = A ⋅ 𝑜 B ⋅ 𝑜 C
49 48 3imp ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω → A ⋅ 𝑜 B ⋅ 𝑜 C = A ⋅ 𝑜 B ⋅ 𝑜 C