---

Step * of Lemma iseg_product-property

∀i,j:ℤ. ∀k:ℕ.  (k | iseg_product(i;j)) supposing ((k ≤ j) and (i ≤ k))
BY
{ (Auto THEN Unfold `iseg_product` 0 THEN BLemma `divides-combinations` THEN Auto') }

---

Latex:

---

Latex:
\mforall{}i,j:\mBbbZ{}.  \mforall{}k:\mBbbN{}.    (k  |  iseg\_product(i;j))  supposing  ((k  \mleq{}  j)  and  (i  \mleq{}  k))


By

---

Latex:
(Auto  THEN  Unfold  `iseg\_product`  0  THEN  BLemma  `divides-combinations`  THEN  Auto')

---

Home Index