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

Proof

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