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 imbitrrid ⊢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