Metamath Proof Explorer

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 𝐶 ) )