---

Step * of Lemma divides-mul

∀x,y,z:ℤ.  (((z | x) ∨ (z | y)) ⇒ (z | (x * y)))
BY
{ (Unfold `divides` 0 THEN Auto THEN D -1 THEN ExRepD THEN HypSubst' -1 0) }

1
1. x : ℤ@i
2. y : ℤ@i
3. z : ℤ@i
4. c : ℤ@i
5. x = (z * c) ∈ ℤ@i
⊢ ∃c@0:ℤ. (((z * c) * y) = (z * c@0) ∈ ℤ)

2
1. x : ℤ@i
2. y : ℤ@i
3. z : ℤ@i
4. c : ℤ@i
5. y = (z * c) ∈ ℤ@i
⊢ ∃c@0:ℤ. ((x * z * c) = (z * c@0) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}x,y,z:\mBbbZ{}.    (((z  |  x)  \mvee{}  (z  |  y))  {}\mRightarrow{}  (z  |  (x  *  y)))


By

---

Latex:
(Unfold  `divides`  0  THEN  Auto  THEN  D  -1  THEN  ExRepD  THEN  HypSubst'  -1  0)

---

Home Index