Proof of Theorem distrpi
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pinn 10918 | . . . 4
⊢ (𝐴 ∈ N →
𝐴 ∈
ω) | 
| 2 |  | pinn 10918 | . . . 4
⊢ (𝐵 ∈ N →
𝐵 ∈
ω) | 
| 3 |  | pinn 10918 | . . . 4
⊢ (𝐶 ∈ N →
𝐶 ∈
ω) | 
| 4 |  | nndi 8661 | . . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ·o (𝐵 +o 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶))) | 
| 5 | 1, 2, 3, 4 | syl3an 1161 | . . 3
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N
∧ 𝐶 ∈
N) → (𝐴
·o (𝐵
+o 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶))) | 
| 6 |  | addclpi 10932 | . . . . . 6
⊢ ((𝐵 ∈ N ∧
𝐶 ∈ N)
→ (𝐵
+N 𝐶) ∈ N) | 
| 7 |  | mulpiord 10925 | . . . . . 6
⊢ ((𝐴 ∈ N ∧
(𝐵
+N 𝐶) ∈ N) → (𝐴
·N (𝐵 +N 𝐶)) = (𝐴 ·o (𝐵 +N 𝐶))) | 
| 8 | 6, 7 | sylan2 593 | . . . . 5
⊢ ((𝐴 ∈ N ∧
(𝐵 ∈ N
∧ 𝐶 ∈
N)) → (𝐴
·N (𝐵 +N 𝐶)) = (𝐴 ·o (𝐵 +N 𝐶))) | 
| 9 |  | addpiord 10924 | . . . . . . 7
⊢ ((𝐵 ∈ N ∧
𝐶 ∈ N)
→ (𝐵
+N 𝐶) = (𝐵 +o 𝐶)) | 
| 10 | 9 | oveq2d 7447 | . . . . . 6
⊢ ((𝐵 ∈ N ∧
𝐶 ∈ N)
→ (𝐴
·o (𝐵
+N 𝐶)) = (𝐴 ·o (𝐵 +o 𝐶))) | 
| 11 | 10 | adantl 481 | . . . . 5
⊢ ((𝐴 ∈ N ∧
(𝐵 ∈ N
∧ 𝐶 ∈
N)) → (𝐴
·o (𝐵
+N 𝐶)) = (𝐴 ·o (𝐵 +o 𝐶))) | 
| 12 | 8, 11 | eqtrd 2777 | . . . 4
⊢ ((𝐴 ∈ N ∧
(𝐵 ∈ N
∧ 𝐶 ∈
N)) → (𝐴
·N (𝐵 +N 𝐶)) = (𝐴 ·o (𝐵 +o 𝐶))) | 
| 13 | 12 | 3impb 1115 | . . 3
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N
∧ 𝐶 ∈
N) → (𝐴
·N (𝐵 +N 𝐶)) = (𝐴 ·o (𝐵 +o 𝐶))) | 
| 14 |  | mulclpi 10933 | . . . . . 6
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ (𝐴
·N 𝐵) ∈ N) | 
| 15 |  | mulclpi 10933 | . . . . . 6
⊢ ((𝐴 ∈ N ∧
𝐶 ∈ N)
→ (𝐴
·N 𝐶) ∈ N) | 
| 16 |  | addpiord 10924 | . . . . . 6
⊢ (((𝐴
·N 𝐵) ∈ N ∧ (𝐴
·N 𝐶) ∈ N) → ((𝐴
·N 𝐵) +N (𝐴
·N 𝐶)) = ((𝐴 ·N 𝐵) +o (𝐴
·N 𝐶))) | 
| 17 | 14, 15, 16 | syl2an 596 | . . . . 5
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐴 ∈
N ∧ 𝐶
∈ N)) → ((𝐴 ·N 𝐵) +N
(𝐴
·N 𝐶)) = ((𝐴 ·N 𝐵) +o (𝐴
·N 𝐶))) | 
| 18 |  | mulpiord 10925 | . . . . . 6
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ (𝐴
·N 𝐵) = (𝐴 ·o 𝐵)) | 
| 19 |  | mulpiord 10925 | . . . . . 6
⊢ ((𝐴 ∈ N ∧
𝐶 ∈ N)
→ (𝐴
·N 𝐶) = (𝐴 ·o 𝐶)) | 
| 20 | 18, 19 | oveqan12d 7450 | . . . . 5
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐴 ∈
N ∧ 𝐶
∈ N)) → ((𝐴 ·N 𝐵) +o (𝐴
·N 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶))) | 
| 21 | 17, 20 | eqtrd 2777 | . . . 4
⊢ (((𝐴 ∈ N ∧
𝐵 ∈ N)
∧ (𝐴 ∈
N ∧ 𝐶
∈ N)) → ((𝐴 ·N 𝐵) +N
(𝐴
·N 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶))) | 
| 22 | 21 | 3impdi 1351 | . . 3
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N
∧ 𝐶 ∈
N) → ((𝐴
·N 𝐵) +N (𝐴
·N 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶))) | 
| 23 | 5, 13, 22 | 3eqtr4d 2787 | . 2
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N
∧ 𝐶 ∈
N) → (𝐴
·N (𝐵 +N 𝐶)) = ((𝐴 ·N 𝐵) +N
(𝐴
·N 𝐶))) | 
| 24 |  | dmaddpi 10930 | . . 3
⊢ dom
+N = (N ×
N) | 
| 25 |  | 0npi 10922 | . . 3
⊢  ¬
∅ ∈ N | 
| 26 |  | dmmulpi 10931 | . . 3
⊢ dom
·N = (N ×
N) | 
| 27 | 24, 25, 26 | ndmovdistr 7622 | . 2
⊢ (¬
(𝐴 ∈ N
∧ 𝐵 ∈
N ∧ 𝐶
∈ N) → (𝐴 ·N (𝐵 +N
𝐶)) = ((𝐴 ·N 𝐵) +N
(𝐴
·N 𝐶))) | 
| 28 | 23, 27 | pm2.61i 182 | 1
⊢ (𝐴
·N (𝐵 +N 𝐶)) = ((𝐴 ·N 𝐵) +N
(𝐴
·N 𝐶)) |