---

Step * of Lemma Legendre-root_wf

∀[n:ℕ]. ∀[i:ℕn].
  (Legendre-root(n;i) ∈ {z:ℝ| (z ∈ (r(-1), r1)) ∧ (Legendre(n;z) = r0) ∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;z)))} )
BY
{ ((Intros THEN Unhide)
   THEN Unfold `Legendre-root` 0
   THEN (Subst' 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)))) 
         ~ TERMOF{Legendre-roots-ext:o, \\v:l} n 0
         THENA (RW (AddrC [2] (TagC (mk_tag_term 2))) 0 THEN Auto)
         )
   THEN GenConclAtAddr [2;1]
   THEN Thin (-1)
   THEN D -1
   THEN ExRepD
   THEN (MemTypeCD THEN Auto)
   THEN (GenConclTerm ⌜v i⌝⋅ THENA Auto)
   THEN (D -2 THEN Unhide)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Intros  THEN  Unhide)
  THEN  Unfold  `Legendre-root`  0
  THEN  (Subst'  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))))\000C 
              \msim{}  TERMOF\{Legendre-roots-ext:o,  \mbackslash{}\mbackslash{}v:l\}  n  0
              THENA  (RW  (AddrC  [2]  (TagC  (mk\_tag\_term  2)))  0  THEN  Auto)
              )
  THEN  GenConclAtAddr  [2;1]
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  ExRepD
  THEN  (MemTypeCD  THEN  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}v  i\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  -2  THEN  Unhide)
  THEN  Auto)

---

Home Index