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 ⊢ A ⋅ 𝑵 B ⋅ 𝑵 C = A ⋅ 𝑵 B ⋅ 𝑵 C

Proof

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