---

Step * 1 of Lemma Legendre-roots-lemma


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)
BY
{ (Assert ∀[x:ℝ]. (Legendre(n - 1;x) = ((r(doublefact((2 * (n - 1)) - 1))/r((n - 1)!)) * rprod(0;n - 2;j.x - z j))) BY
         ((D 0 THENA Auto)
          THEN (InstLemma `Legendre-rpolynomial` [⌜n - 1⌝]⋅ THENA Auto)
          THEN D -1
          THEN (InstLemma `rpolynomial-complete-factors-ordered` [⌜n - 1⌝;⌜a⌝;⌜z⌝]⋅
                THENA (Auto THEN RWO "-3<" 0 THEN Auto)
                )
          THEN D -2
          THEN (RWW "-3 -1" 0 THENA Auto)
          THEN (Subst' n - 1 - 1 ~ n - 2 0 THENA Auto)
          THEN RWO  "-2" 0
          THEN Auto)) }

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
9. ∀[x:ℝ]. (Legendre(n - 1;x) = ((r(doublefact((2 * (n - 1)) - 1))/r((n - 1)!)) * rprod(0;n - 2;j.x - z j)))
⊢ r0 < -(Legendre(n - 1;v) * r(n) * r(-1)^n - i)

---

Latex:

---

Latex:

1.  n  :  \{2...\}
2.  z  :  \mBbbN{}n  -  1  {}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  (r(-1),  r1)\} 
3.  \mforall{}i:\mBbbN{}n  -  1.  (Legendre(n  -  1;z  i)  =  r0)
4.  \mforall{}i:\mBbbN{}n  -  2.  ((z  i)  <  (z  (i  +  1)))
5.  i  :  \mBbbN{}n
6.  v  :  \mBbbR{}
7.  v  \mmember{}  (if  i=0  then  r(-1)  else  (z  (i  -  1)),  if  i=n  -  1  then  r1  else  (z  i))
8.  Legendre(n;v)  =  r0
\mvdash{}  r0  <  -(Legendre(n  -  1;v)  *  r(n)  *  r(-1)\^{}n  -  i)


By

---

Latex:
(Assert  \mforall{}[x:\mBbbR{}]
                    (Legendre(n  -  1;x)
                    =  ((r(doublefact((2  *  (n  -  1))  -  1))/r((n  -  1)!))  *  rprod(0;n  -  2;j.x  -  z  j)))  BY
              ((D  0  THENA  Auto)
                THEN  (InstLemma  `Legendre-rpolynomial`  [\mkleeneopen{}n  -  1\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  D  -1
                THEN  (InstLemma  `rpolynomial-complete-factors-ordered`  [\mkleeneopen{}n  -  1\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}
                            THENA  (Auto  THEN  RWO  "-3<"  0  THEN  Auto)
                            )
                THEN  D  -2
                THEN  (RWW  "-3  -1"  0  THENA  Auto)
                THEN  (Subst'  n  -  1  -  1  \msim{}  n  -  2  0  THENA  Auto)
                THEN  RWO    "-2"  0
                THEN  Auto))

---

Home Index