Metamath Proof Explorer

Theorem distrpi

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

Ref Expression
Assertion distrpi ⊢A⋅𝑵B+𝑵C=A⋅𝑵B+𝑵A⋅𝑵C

Proof

Step Hyp Ref Expression
1 pinn ⊢A∈𝑵→A∈ω
2 pinn ⊢B∈𝑵→B∈ω
3 pinn ⊢C∈𝑵→C∈ω
4 nndi ⊢A∈ω∧B∈ω∧C∈ω→A⋅𝑜B+𝑜C=A⋅𝑜B+𝑜A⋅𝑜C
5 1 2 3 4 syl3an ⊢A∈𝑵∧B∈𝑵∧C∈𝑵→A⋅𝑜B+𝑜C=A⋅𝑜B+𝑜A⋅𝑜C
6 addclpi ⊢B∈𝑵∧C∈𝑵→B+𝑵C∈𝑵
7 mulpiord ⊢A∈𝑵∧B+𝑵C∈𝑵→A⋅𝑵B+𝑵C=A⋅𝑜B+𝑵C
8 6 7 sylan2 ⊢A∈𝑵∧B∈𝑵∧C∈𝑵→A⋅𝑵B+𝑵C=A⋅𝑜B+𝑵C
9 addpiord ⊢B∈𝑵∧C∈𝑵→B+𝑵C=B+𝑜C
10 9 oveq2d ⊢B∈𝑵∧C∈𝑵→A⋅𝑜B+𝑵C=A⋅𝑜B+𝑜C
11 10 adantl ⊢A∈𝑵∧B∈𝑵∧C∈𝑵→A⋅𝑜B+𝑵C=A⋅𝑜B+𝑜C
12 8 11 eqtrd ⊢A∈𝑵∧B∈𝑵∧C∈𝑵→A⋅𝑵B+𝑵C=A⋅𝑜B+𝑜C
13 12 3impb ⊢A∈𝑵∧B∈𝑵∧C∈𝑵→A⋅𝑵B+𝑵C=A⋅𝑜B+𝑜C
14 mulclpi ⊢A∈𝑵∧B∈𝑵→A⋅𝑵B∈𝑵
15 mulclpi ⊢A∈𝑵∧C∈𝑵→A⋅𝑵C∈𝑵
16 addpiord ⊢A⋅𝑵B∈𝑵∧A⋅𝑵C∈𝑵→A⋅𝑵B+𝑵A⋅𝑵C=A⋅𝑵B+𝑜A⋅𝑵C
17 14 15 16 syl2an ⊢A∈𝑵∧B∈𝑵∧A∈𝑵∧C∈𝑵→A⋅𝑵B+𝑵A⋅𝑵C=A⋅𝑵B+𝑜A⋅𝑵C
18 mulpiord ⊢A∈𝑵∧B∈𝑵→A⋅𝑵B=A⋅𝑜B
19 mulpiord ⊢A∈𝑵∧C∈𝑵→A⋅𝑵C=A⋅𝑜C
20 18 19 oveqan12d ⊢A∈𝑵∧B∈𝑵∧A∈𝑵∧C∈𝑵→A⋅𝑵B+𝑜A⋅𝑵C=A⋅𝑜B+𝑜A⋅𝑜C
21 17 20 eqtrd ⊢A∈𝑵∧B∈𝑵∧A∈𝑵∧C∈𝑵→A⋅𝑵B+𝑵A⋅𝑵C=A⋅𝑜B+𝑜A⋅𝑜C
22 21 3impdi ⊢A∈𝑵∧B∈𝑵∧C∈𝑵→A⋅𝑵B+𝑵A⋅𝑵C=A⋅𝑜B+𝑜A⋅𝑜C
23 5 13 22 3eqtr4d ⊢A∈𝑵∧B∈𝑵∧C∈𝑵→A⋅𝑵B+𝑵C=A⋅𝑵B+𝑵A⋅𝑵C
24 dmaddpi ⊢dom⁡+𝑵=𝑵×𝑵
25 0npi ⊢¬∅∈𝑵
26 dmmulpi ⊢dom⁡⋅𝑵=𝑵×𝑵
27 24 25 26 ndmovdistr ⊢¬A∈𝑵∧B∈𝑵∧C∈𝑵→A⋅𝑵B+𝑵C=A⋅𝑵B+𝑵A⋅𝑵C
28 23 27 pm2.61i ⊢A⋅𝑵B+𝑵C=A⋅𝑵B+𝑵A⋅𝑵C