Theorem mulasspi

Description: Multiplication of positive integers is associative. (Contributed by NM, 21-Sep-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	mulasspi	⊢ ( ( 𝐴 ·N 𝐵 ) ·N 𝐶 ) = ( 𝐴 ·N ( 𝐵 ·N 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		pinn	⊢ ( 𝐴 ∈ N → 𝐴 ∈ ω )
2		pinn	⊢ ( 𝐵 ∈ N → 𝐵 ∈ ω )
3		pinn	⊢ ( 𝐶 ∈ N → 𝐶 ∈ ω )
4		nnmass	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 𝐴 ·o 𝐵 ) ·o 𝐶 ) = ( 𝐴 ·o ( 𝐵 ·o 𝐶 ) ) )
5	1 2 3 4	syl3an	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( ( 𝐴 ·o 𝐵 ) ·o 𝐶 ) = ( 𝐴 ·o ( 𝐵 ·o 𝐶 ) ) )
6		mulclpi	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 ·N 𝐵 ) ∈ N )
7		mulpiord	⊢ ( ( ( 𝐴 ·N 𝐵 ) ∈ N ∧ 𝐶 ∈ N ) → ( ( 𝐴 ·N 𝐵 ) ·N 𝐶 ) = ( ( 𝐴 ·N 𝐵 ) ·o 𝐶 ) )
8	6 7	sylan	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( ( 𝐴 ·N 𝐵 ) ·N 𝐶 ) = ( ( 𝐴 ·N 𝐵 ) ·o 𝐶 ) )
9		mulpiord	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 ·N 𝐵 ) = ( 𝐴 ·o 𝐵 ) )
10	9	oveq1d	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( ( 𝐴 ·N 𝐵 ) ·o 𝐶 ) = ( ( 𝐴 ·o 𝐵 ) ·o 𝐶 ) )
11	10	adantr	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( ( 𝐴 ·N 𝐵 ) ·o 𝐶 ) = ( ( 𝐴 ·o 𝐵 ) ·o 𝐶 ) )
12	8 11	eqtrd	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( ( 𝐴 ·N 𝐵 ) ·N 𝐶 ) = ( ( 𝐴 ·o 𝐵 ) ·o 𝐶 ) )
13	12	3impa	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( ( 𝐴 ·N 𝐵 ) ·N 𝐶 ) = ( ( 𝐴 ·o 𝐵 ) ·o 𝐶 ) )
14		mulclpi	⊢ ( ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐵 ·N 𝐶 ) ∈ N )
15		mulpiord	⊢ ( ( 𝐴 ∈ N ∧ ( 𝐵 ·N 𝐶 ) ∈ N ) → ( 𝐴 ·N ( 𝐵 ·N 𝐶 ) ) = ( 𝐴 ·o ( 𝐵 ·N 𝐶 ) ) )
16	14 15	sylan2	⊢ ( ( 𝐴 ∈ N ∧ ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) ) → ( 𝐴 ·N ( 𝐵 ·N 𝐶 ) ) = ( 𝐴 ·o ( 𝐵 ·N 𝐶 ) ) )
17		mulpiord	⊢ ( ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐵 ·N 𝐶 ) = ( 𝐵 ·o 𝐶 ) )
18	17	oveq2d	⊢ ( ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐴 ·o ( 𝐵 ·N 𝐶 ) ) = ( 𝐴 ·o ( 𝐵 ·o 𝐶 ) ) )
19	18	adantl	⊢ ( ( 𝐴 ∈ N ∧ ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) ) → ( 𝐴 ·o ( 𝐵 ·N 𝐶 ) ) = ( 𝐴 ·o ( 𝐵 ·o 𝐶 ) ) )
20	16 19	eqtrd	⊢ ( ( 𝐴 ∈ N ∧ ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) ) → ( 𝐴 ·N ( 𝐵 ·N 𝐶 ) ) = ( 𝐴 ·o ( 𝐵 ·o 𝐶 ) ) )
21	20	3impb	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐴 ·N ( 𝐵 ·N 𝐶 ) ) = ( 𝐴 ·o ( 𝐵 ·o 𝐶 ) ) )
22	5 13 21	3eqtr4d	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( ( 𝐴 ·N 𝐵 ) ·N 𝐶 ) = ( 𝐴 ·N ( 𝐵 ·N 𝐶 ) ) )
23		dmmulpi	⊢ dom ·N = ( N × N )
24		0npi	⊢ ¬ ∅ ∈ N
25	23 24	ndmovass	⊢ ( ¬ ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( ( 𝐴 ·N 𝐵 ) ·N 𝐶 ) = ( 𝐴 ·N ( 𝐵 ·N 𝐶 ) ) )
26	22 25	pm2.61i	⊢ ( ( 𝐴 ·N 𝐵 ) ·N 𝐶 ) = ( 𝐴 ·N ( 𝐵 ·N 𝐶 ) )