---

Step * of Lemma Legendre-roots-lemma

∀n:{2...}. ∀z:ℕn - 1 ⟶ {x:ℝ| x ∈ (r(-1), r1)} .
  ((∀i:ℕn - 1. (Legendre(n - 1;z i) = r0))
  ⇒ (∀i:ℕn - 2. ((z i) < (z (i + 1))))
  ⇒ (∀i:ℕn. ∀v:{v:ℝ| (v ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i))) ∧ (Legendre(n;v) = r0)} \000C.
        (r0 < (r(-1)^n - i * Legendre(n + 1;v)))))
BY
{ (Auto
   THEN DSetVars
   THEN (Unhide THENA Auto)
   THEN ExRepD
   THEN Unfold `Legendre` 0
   THEN (Subst' (n + 1 =z 0) ~ ff 0 THENA Auto)
   THEN (Subst' (n + 1 =z 1) ~ ff 0 THENA Auto)
   THEN (Subst' (n + 1) - 1 ~ n 0 THENA Auto)
   THEN (Subst' (n + 1) - 2 ~ n - 1 0 THENA Auto)
   THEN Reduce 0
   THEN (RWO "-1" 0 THENA Auto)
   THEN (RWW "int-rdiv-req int-rmul-req" 0 THENA Auto)
   THEN nRMul ⌜r(n + 1)⌝ 0⋅) }

1
1. n : {2...}
2. z : ℕn - 1 ⟶ {x:ℝ| x ∈ (r(-1), r1)} 
3. ∀i:ℕn - 1. (Legendre(n - 1;z i) = r0)
4. ∀i:ℕn - 2. ((z i) < (z (i + 1)))
5. i : ℕn
6. v : ℝ
7. v ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i))
8. Legendre(n;v) = r0
⊢ r0 < -(Legendre(n - 1;v) * r(n) * r(-1)^n - i)

---

Latex:

---

Latex:
\mforall{}n:\{2...\}.  \mforall{}z:\mBbbN{}n  -  1  {}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  (r(-1),  r1)\}  .
    ((\mforall{}i:\mBbbN{}n  -  1.  (Legendre(n  -  1;z  i)  =  r0))
    {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n  -  2.  ((z  i)  <  (z  (i  +  1))))
    {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n.  \mforall{}v:\{v:\mBbbR{}| 
                                  (v  \mmember{}  (if  i=0  then  r(-1)  else  (z  (i  -  1)),  if  i=n  -  1  then  r1  else  (z  i)))
                                  \mwedge{}  (Legendre(n;v)  =  r0)\}  .
                (r0  <  (r(-1)\^{}n  -  i  *  Legendre(n  +  1;v)))))


By

---

Latex:
(Auto
  THEN  DSetVars
  THEN  (Unhide  THENA  Auto)
  THEN  ExRepD
  THEN  Unfold  `Legendre`  0
  THEN  (Subst'  (n  +  1  =\msubz{}  0)  \msim{}  ff  0  THENA  Auto)
  THEN  (Subst'  (n  +  1  =\msubz{}  1)  \msim{}  ff  0  THENA  Auto)
  THEN  (Subst'  (n  +  1)  -  1  \msim{}  n  0  THENA  Auto)
  THEN  (Subst'  (n  +  1)  -  2  \msim{}  n  -  1  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (RWW  "int-rdiv-req  int-rmul-req"  0  THENA  Auto)
  THEN  nRMul  \mkleeneopen{}r(n  +  1)\mkleeneclose{}  0\mcdot{})

---

Home Index