---

Step * of Lemma divides_transitivity

∀a,b,c:ℤ.  ((a | b) ⇒ (b | c) ⇒ (a | c))
BY
{ (Unfold `divides` 0 THEN Auto) }

1
1. a : ℤ
2. b : ℤ
3. c : ℤ
4. ∃c:ℤ. (b = (a * c) ∈ ℤ)
5. ∃c@0:ℤ. (c = (b * c@0) ∈ ℤ)
⊢ ∃c@0:ℤ. (c = (a * c@0) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}a,b,c:\mBbbZ{}.    ((a  |  b)  {}\mRightarrow{}  (b  |  c)  {}\mRightarrow{}  (a  |  c))


By

---

Latex:
(Unfold  `divides`  0  THEN  Auto)

---

Home Index