---

Step * 1 1 1 1 2 1 1 of Lemma Legendre-roots-sq

.....aux..... 
1. n : ℤ
2. z : i:ℕn - 1 ⟶ {x:ℝ| (x ∈ (r(-1), r1)) ∧ (Legendre(n - 1;x) = r0) ∧ (r0 < (r((-1)^(n - 1 - i)) * Legendre(n;x)))} 
3. ∀i:ℕn - 2. ((z i) < (z (i + 1)))
4. 2 ≤ n
5. ∀a,b:ℝ.  rational_fun_zero(λx.ratLegendre(n;x);a;b) ∈ {c:ℝ| (c ∈ (a, b)) ∧ (Legendre(n;c) = r0)}  supposing (a < b) ∧\000C ((Legendre(n;a) * Legendre(n;b)) < r0)
6. i : ℕn
7. i = 0 ∈ ℤ
⊢ r0 < (r((-1)^(n - i)) * Legendre(n;r(-1)))
BY
{ ((Subst' n - i ~ n 0 THENA Auto)
   THEN (RWO "Legendre-minus-1" 0 THENA Auto)
   THEN (RWW  "rmul-int exp_add<" 0 THENA Auto)
   THEN (Subst' n + n ~ 2 * n 0 THENA Auto)
   THEN (RWW "exp-minusone mod2-2n" 0 THENA Auto)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
.....aux..... 
1.  n  :  \mBbbZ{}
2.  z  :  i:\mBbbN{}n  -  1  {}\mrightarrow{}  \{x:\mBbbR{}| 
                                        (x  \mmember{}  (r(-1),  r1))
                                        \mwedge{}  (Legendre(n  -  1;x)  =  r0)
                                        \mwedge{}  (r0  <  (r((-1)\^{}(n  -  1  -  i))  *  Legendre(n;x)))\} 
3.  \mforall{}i:\mBbbN{}n  -  2.  ((z  i)  <  (z  (i  +  1)))
4.  2  \mleq{}  n
5.  \mforall{}a,b:\mBbbR{}.
          rational\_fun\_zero(\mlambda{}x.ratLegendre(n;x);a;b)  \mmember{}  \{c:\mBbbR{}|  (c  \mmember{}  (a,  b))  \mwedge{}  (Legendre(n;c)  =  r0)\}   
          supposing  (a  <  b)  \mwedge{}  ((Legendre(n;a)  *  Legendre(n;b))  <  r0)
6.  i  :  \mBbbN{}n
7.  i  =  0
\mvdash{}  r0  <  (r((-1)\^{}(n  -  i))  *  Legendre(n;r(-1)))


By

---

Latex:
((Subst'  n  -  i  \msim{}  n  0  THENA  Auto)
  THEN  (RWO  "Legendre-minus-1"  0  THENA  Auto)
  THEN  (RWW    "rmul-int  exp\_add<"  0  THENA  Auto)
  THEN  (Subst'  n  +  n  \msim{}  2  *  n  0  THENA  Auto)
  THEN  (RWW  "exp-minusone  mod2-2n"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index