---

Step * of Lemma LegendreSigns_wf

∀[n:ℕ]. ∀[L:(x:ℤ × ℕ+ × {s:{-1..2-}| s = ratsign(ratLegendre(n;x)) ∈ ℤ} ) List].
  (LegendreSigns(n;L) ∈ (x:ℤ × ℕ+ × {s:{-1..2-}| s = ratsign(ratLegendre(n;x)) ∈ ℤ} ) List)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[L:(x:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}  \mtimes{}  \{s:\{-1..2\msupminus{}\}|  s  =  ratsign(ratLegendre(n;x))\}  )  List].
    (LegendreSigns(n;L)  \mmember{}  (x:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}  \mtimes{}  \{s:\{-1..2\msupminus{}\}|  s  =  ratsign(ratLegendre(n;x))\}  )  List)


By

---

Latex:
ProveWfLemma

---

Home Index