---

Step * of Lemma Legendre-roots-ext

∀n:ℕ
  (∃z:i:ℕn ⟶ {x:ℝ| (x ∈ (r(-1), r1)) ∧ (Legendre(n;x) = r0) ∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))} 
  [(∀i:ℕn - 1. ((z i) < (z (i + 1))))])
BY
{ Extract of Obid: Legendre-roots-sq
  not unfolding  rational_fun_zero primrec rsqrt int-rdiv int-rmul rminus int-to-real ratLegendre
  finishing with Auto
  normalizes to:
  
  λn.primrec(n;λi.r0;λi,x. if i + 1=1
                           then λi.r0
                           else (λi@0.rational_fun_zero(λx.ratLegendre(i + 1;x);if i@0=0
                                                                                then r(-1)
                                                                                else (x (i@0 - 1));if i@0=(i + 1) - 1
                                                                                                   then r1
                                                                                                   else (x i@0)))) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}
    (\mexists{}z:i:\mBbbN{}n  {}\mrightarrow{}  \{x:\mBbbR{}| 
                              (x  \mmember{}  (r(-1),  r1))
                              \mwedge{}  (Legendre(n;x)  =  r0)
                              \mwedge{}  (r0  <  (r((-1)\^{}(n  -  i))  *  Legendre(n  +  1;x)))\}    [(\mforall{}i:\mBbbN{}n  -  1.  ((z  i)  <  (z  (i  +  1))))]\000C)


By

---

Latex:
Extract  of  Obid:  Legendre-roots-sq
not  unfolding    rational\_fun\_zero  primrec  rsqrt  int-rdiv  int-rmul  rminus  int-to-real  ratLegendre
finishing  with  Auto
normalizes  to:

\mlambda{}n.primrec(n;\mlambda{}i.r0;\mlambda{}i,x.  if  i  +  1=1
                                                  then  \mlambda{}i.r0
                                                  else  (\mlambda{}i@0.rational\_fun\_zero(\mlambda{}x.ratLegendre(i
                                                                                                                  +  1;x);if  i@0=0
                                                                                                                                then  r(-1)
                                                                                                                                else  (x  (i@0  -  1));if  i@0=(i  +  1) 
                                                                                                                                                                      -  1
                                                                                                                                                                      then  r1
                                                                                                                                                                      else  (x  i@0))))

---

Home Index