---

Step * of Lemma iseg_product-split

∀[i,j,k:ℤ].  (iseg_product(i;j) ~ iseg_product(i;k) * iseg_product(k + 1;j)) supposing (k < j and (i ≤ k) and (1 ≤ i))
BY
{ (Auto
   THEN Unfold `iseg_product` 0
   THEN (InstLemma `combinations-split` [⌜j⌝;⌜(k - i) + 1⌝;⌜(j - k + 1) + 1⌝]⋅ THENA Auto')
   THEN (RW IntNormC (-1) THENM RW IntNormC 0)
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[i,j,k:\mBbbZ{}].
    (iseg\_product(i;j)  \msim{}  iseg\_product(i;k)  *  iseg\_product(k  +  1;j))  supposing 
          (k  <  j  and 
          (i  \mleq{}  k)  and 
          (1  \mleq{}  i))


By

---

Latex:
(Auto
  THEN  Unfold  `iseg\_product`  0
  THEN  (InstLemma  `combinations-split`  [\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}(k  -  i)  +  1\mkleeneclose{};\mkleeneopen{}(j  -  k  +  1)  +  1\mkleeneclose{}]\mcdot{}  THENA  Auto')
  THEN  (RW  IntNormC  (-1)  THENM  RW  IntNormC  0)
  THEN  Auto')

---

Home Index