---

Step * of Lemma Legendre-roots-unique

∀[n:ℕ]. ∀[z:ℕn ⟶ ℝ].
  (∀[i:ℕn]. ((z i) = Legendre-root(n;i))) supposing 
     ((∀i:ℕn. (Legendre(n;z i) = r0)) and 
     (∀i:ℕn - 1. ((z i) < (z (i + 1)))))
BY
{ (Auto THEN (InstLemma `Legendre-rpolynomial` [⌜n⌝]⋅ THENA Auto) THEN ExRepD) }

1
1. n : ℕ
2. z : ℕn ⟶ ℝ
3. ∀i:ℕn - 1. ((z i) < (z (i + 1)))
4. ∀i:ℕn. (Legendre(n;z i) = r0)
5. i : ℕn
6. a : ℕn + 1 ⟶ ℝ
7. ∀x:ℝ. (Legendre(n;x) = (Σi≤n. a_i * x^i))
8. (a n) = (r(doublefact((2 * n) - 1))/r((n)!))
⊢ (z i) = Legendre-root(n;i)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[z:\mBbbN{}n  {}\mrightarrow{}  \mBbbR{}].
    (\mforall{}[i:\mBbbN{}n].  ((z  i)  =  Legendre-root(n;i)))  supposing 
          ((\mforall{}i:\mBbbN{}n.  (Legendre(n;z  i)  =  r0))  and 
          (\mforall{}i:\mBbbN{}n  -  1.  ((z  i)  <  (z  (i  +  1)))))


By

---

Latex:
(Auto  THEN  (InstLemma  `Legendre-rpolynomial`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)

---

Home Index