# 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}{\cdot }_{𝑵}\left({B}{+}_{𝑵}{C}\right)=\left({A}{\cdot }_{𝑵}{B}\right){+}_{𝑵}\left({A}{\cdot }_{𝑵}{C}\right)$

### Proof

Step Hyp Ref Expression
1 pinn ${⊢}{A}\in 𝑵\to {A}\in \mathrm{\omega }$
2 pinn ${⊢}{B}\in 𝑵\to {B}\in \mathrm{\omega }$
3 pinn ${⊢}{C}\in 𝑵\to {C}\in \mathrm{\omega }$
4 nndi ${⊢}\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\wedge {C}\in \mathrm{\omega }\right)\to {A}{\cdot }_{𝑜}\left({B}{+}_{𝑜}{C}\right)=\left({A}{\cdot }_{𝑜}{B}\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{C}\right)$
5 1 2 3 4 syl3an ${⊢}\left({A}\in 𝑵\wedge {B}\in 𝑵\wedge {C}\in 𝑵\right)\to {A}{\cdot }_{𝑜}\left({B}{+}_{𝑜}{C}\right)=\left({A}{\cdot }_{𝑜}{B}\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{C}\right)$
6 addclpi ${⊢}\left({B}\in 𝑵\wedge {C}\in 𝑵\right)\to {B}{+}_{𝑵}{C}\in 𝑵$
7 mulpiord ${⊢}\left({A}\in 𝑵\wedge {B}{+}_{𝑵}{C}\in 𝑵\right)\to {A}{\cdot }_{𝑵}\left({B}{+}_{𝑵}{C}\right)={A}{\cdot }_{𝑜}\left({B}{+}_{𝑵}{C}\right)$
8 6 7 sylan2 ${⊢}\left({A}\in 𝑵\wedge \left({B}\in 𝑵\wedge {C}\in 𝑵\right)\right)\to {A}{\cdot }_{𝑵}\left({B}{+}_{𝑵}{C}\right)={A}{\cdot }_{𝑜}\left({B}{+}_{𝑵}{C}\right)$
9 addpiord ${⊢}\left({B}\in 𝑵\wedge {C}\in 𝑵\right)\to {B}{+}_{𝑵}{C}={B}{+}_{𝑜}{C}$
10 9 oveq2d ${⊢}\left({B}\in 𝑵\wedge {C}\in 𝑵\right)\to {A}{\cdot }_{𝑜}\left({B}{+}_{𝑵}{C}\right)={A}{\cdot }_{𝑜}\left({B}{+}_{𝑜}{C}\right)$
11 10 adantl ${⊢}\left({A}\in 𝑵\wedge \left({B}\in 𝑵\wedge {C}\in 𝑵\right)\right)\to {A}{\cdot }_{𝑜}\left({B}{+}_{𝑵}{C}\right)={A}{\cdot }_{𝑜}\left({B}{+}_{𝑜}{C}\right)$
12 8 11 eqtrd ${⊢}\left({A}\in 𝑵\wedge \left({B}\in 𝑵\wedge {C}\in 𝑵\right)\right)\to {A}{\cdot }_{𝑵}\left({B}{+}_{𝑵}{C}\right)={A}{\cdot }_{𝑜}\left({B}{+}_{𝑜}{C}\right)$
13 12 3impb ${⊢}\left({A}\in 𝑵\wedge {B}\in 𝑵\wedge {C}\in 𝑵\right)\to {A}{\cdot }_{𝑵}\left({B}{+}_{𝑵}{C}\right)={A}{\cdot }_{𝑜}\left({B}{+}_{𝑜}{C}\right)$
14 mulclpi ${⊢}\left({A}\in 𝑵\wedge {B}\in 𝑵\right)\to {A}{\cdot }_{𝑵}{B}\in 𝑵$
15 mulclpi ${⊢}\left({A}\in 𝑵\wedge {C}\in 𝑵\right)\to {A}{\cdot }_{𝑵}{C}\in 𝑵$
16 addpiord ${⊢}\left({A}{\cdot }_{𝑵}{B}\in 𝑵\wedge {A}{\cdot }_{𝑵}{C}\in 𝑵\right)\to \left({A}{\cdot }_{𝑵}{B}\right){+}_{𝑵}\left({A}{\cdot }_{𝑵}{C}\right)=\left({A}{\cdot }_{𝑵}{B}\right){+}_{𝑜}\left({A}{\cdot }_{𝑵}{C}\right)$
17 14 15 16 syl2an ${⊢}\left(\left({A}\in 𝑵\wedge {B}\in 𝑵\right)\wedge \left({A}\in 𝑵\wedge {C}\in 𝑵\right)\right)\to \left({A}{\cdot }_{𝑵}{B}\right){+}_{𝑵}\left({A}{\cdot }_{𝑵}{C}\right)=\left({A}{\cdot }_{𝑵}{B}\right){+}_{𝑜}\left({A}{\cdot }_{𝑵}{C}\right)$
18 mulpiord ${⊢}\left({A}\in 𝑵\wedge {B}\in 𝑵\right)\to {A}{\cdot }_{𝑵}{B}={A}{\cdot }_{𝑜}{B}$
19 mulpiord ${⊢}\left({A}\in 𝑵\wedge {C}\in 𝑵\right)\to {A}{\cdot }_{𝑵}{C}={A}{\cdot }_{𝑜}{C}$
20 18 19 oveqan12d ${⊢}\left(\left({A}\in 𝑵\wedge {B}\in 𝑵\right)\wedge \left({A}\in 𝑵\wedge {C}\in 𝑵\right)\right)\to \left({A}{\cdot }_{𝑵}{B}\right){+}_{𝑜}\left({A}{\cdot }_{𝑵}{C}\right)=\left({A}{\cdot }_{𝑜}{B}\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{C}\right)$
21 17 20 eqtrd ${⊢}\left(\left({A}\in 𝑵\wedge {B}\in 𝑵\right)\wedge \left({A}\in 𝑵\wedge {C}\in 𝑵\right)\right)\to \left({A}{\cdot }_{𝑵}{B}\right){+}_{𝑵}\left({A}{\cdot }_{𝑵}{C}\right)=\left({A}{\cdot }_{𝑜}{B}\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{C}\right)$
22 21 3impdi ${⊢}\left({A}\in 𝑵\wedge {B}\in 𝑵\wedge {C}\in 𝑵\right)\to \left({A}{\cdot }_{𝑵}{B}\right){+}_{𝑵}\left({A}{\cdot }_{𝑵}{C}\right)=\left({A}{\cdot }_{𝑜}{B}\right){+}_{𝑜}\left({A}{\cdot }_{𝑜}{C}\right)$
23 5 13 22 3eqtr4d ${⊢}\left({A}\in 𝑵\wedge {B}\in 𝑵\wedge {C}\in 𝑵\right)\to {A}{\cdot }_{𝑵}\left({B}{+}_{𝑵}{C}\right)=\left({A}{\cdot }_{𝑵}{B}\right){+}_{𝑵}\left({A}{\cdot }_{𝑵}{C}\right)$
24 dmaddpi ${⊢}\mathrm{dom}{+}_{𝑵}=𝑵×𝑵$
25 0npi ${⊢}¬\varnothing \in 𝑵$
26 dmmulpi ${⊢}\mathrm{dom}{\cdot }_{𝑵}=𝑵×𝑵$
27 24 25 26 ndmovdistr ${⊢}¬\left({A}\in 𝑵\wedge {B}\in 𝑵\wedge {C}\in 𝑵\right)\to {A}{\cdot }_{𝑵}\left({B}{+}_{𝑵}{C}\right)=\left({A}{\cdot }_{𝑵}{B}\right){+}_{𝑵}\left({A}{\cdot }_{𝑵}{C}\right)$
28 23 27 pm2.61i ${⊢}{A}{\cdot }_{𝑵}\left({B}{+}_{𝑵}{C}\right)=\left({A}{\cdot }_{𝑵}{B}\right){+}_{𝑵}\left({A}{\cdot }_{𝑵}{C}\right)$