---

Step * 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)!))
⊢ (z i) = Legendre-root(n;i)
BY
{ Assert ⌜r0 < (a n)⌝⋅ }

1
.....assertion..... 
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)!))
⊢ r0 < (a n)

2
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)
⊢ (z i) = Legendre-root(n;i)

---

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)!))
\mvdash{}  (z  i)  =  Legendre-root(n;i)


By

---

Latex:
Assert  \mkleeneopen{}r0  <  (a  n)\mkleeneclose{}\mcdot{}

---

Home Index