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