---

Step * of Lemma iseg_product_rem_property

∀[k,j:ℕ]. ∀[i:ℕj + 1].  iseg_product_rem(i;j;k) = (iseg_product(i;j) rem k) ∈ ℤ supposing 1 < k
BY
{ xxx(Auto
      THEN RepUR ``iseg_product_rem iseg_product combinations`` 0
      THEN (RWO "combinations_aux_rem_property<" 0 THENM EqCD)
      THEN Auto')xxx }

---

Latex:

---

Latex:
\mforall{}[k,j:\mBbbN{}].  \mforall{}[i:\mBbbN{}j  +  1].    iseg\_product\_rem(i;j;k)  =  (iseg\_product(i;j)  rem  k)  supposing  1  <  k


By

---

Latex:
xxx(Auto
        THEN  RepUR  ``iseg\_product\_rem  iseg\_product  combinations``  0
        THEN  (RWO  "combinations\_aux\_rem\_property<"  0  THENM  EqCD)
        THEN  Auto')xxx

---

Home Index