---

Step * of Lemma divides_product

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

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

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

---

Latex:

---

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


By

---

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

---

Home Index