---

Step * of Lemma iseg_product_rem_wf

∀[k:ℕ+]. ∀[j:ℕ]. ∀[i:ℕj + 1].  (iseg_product_rem(i;j;k) ∈ ℕ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[j:\mBbbN{}].  \mforall{}[i:\mBbbN{}j  +  1].    (iseg\_product\_rem(i;j;k)  \mmember{}  \mBbbN{})


By

---

Latex:
ProveWfLemma

---

Home Index