---

Step * 1 2 2 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
⊢ (Σi≤n. a_i * Legendre-root(n;j)^i) = r0
BY
{ ((RWO "7<" 0 THENA Auto) THEN GenConclTerm ⌜Legendre-root(n;j)⌝⋅ 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
\mvdash{}  (\mSigma{}i\mleq{}n.  a\_i  *  Legendre-root(n;j)\^{}i)  =  r0


By

---

Latex:
((RWO  "7<"  0  THENA  Auto)  THEN  GenConclTerm  \mkleeneopen{}Legendre-root(n;j)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index