---

Step * 1 2 1 of Lemma Legendre-roots-unique


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)!))
9. r0 < (a n)
10. ∀i:ℕn. ((Σi≤n. a_i * z i^i) = r0)
11. j : ℕn - 1
⊢ Legendre-root(n;j) < Legendre-root(n;j + 1)
BY
{ (BLemma `Legendre-roots-rless` THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  z  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbR{}
3.  \mforall{}i:\mBbbN{}n  -  1.  ((z  i)  <  (z  (i  +  1)))
4.  \mforall{}i:\mBbbN{}n.  (Legendre(n;z  i)  =  r0)
5.  i  :  \mBbbN{}n
6.  a  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}
7.  \mforall{}x:\mBbbR{}.  (Legendre(n;x)  =  (\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i))
8.  (a  n)  =  (r(doublefact((2  *  n)  -  1))/r((n)!))
9.  r0  <  (a  n)
10.  \mforall{}i:\mBbbN{}n.  ((\mSigma{}i\mleq{}n.  a\_i  *  z  i\^{}i)  =  r0)
11.  j  :  \mBbbN{}n  -  1
\mvdash{}  Legendre-root(n;j)  <  Legendre-root(n;j  +  1)


By

---

Latex:
(BLemma  `Legendre-roots-rless`  THEN  Auto)

---

Home Index