---

Step * 1 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)
⊢ (z i) = Legendre-root(n;i)
BY
{ ((DupHyp 4 THEN (RWO  "-4" (-1) THENA Auto))
   THEN (InstLemma `rpolynomial-complete-roots-unique` [⌜n⌝;⌜a⌝;⌜z⌝;⌜λi.Legendre-root(n;i)⌝;⌜i⌝]⋅
         THENA (Reduce 0 THEN Auto)
         )
   ) }

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)!))
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)

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)
10. ∀i:ℕn. ((Σi≤n. a_i * z i^i) = r0)
11. j : ℕn
⊢ (Σi≤n. a_i * Legendre-root(n;j)^i) = r0

3
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. (z i) = ((λi.Legendre-root(n;i)) i)
⊢ (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)!))
9.  r0  <  (a  n)
\mvdash{}  (z  i)  =  Legendre-root(n;i)


By

---

Latex:
((DupHyp  4  THEN  (RWO    "-4"  (-1)  THENA  Auto))
  THEN  (InstLemma  `rpolynomial-complete-roots-unique`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}\mlambda{}i.Legendre-root(n;i)\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}
              THENA  (Reduce  0  THEN  Auto)
              )
  )

---

Home Index