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