---

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


1. n : ℤ
2. z : i:ℕn - 1 ⟶ {x:ℝ| 
                    ((r(-1) < x) ∧ (x < r1))
                    ∧ (Legendre(n - 1;x) = r0)
                    ∧ (r0 < (r((-1)^(n - 1 - i)) * Legendre((n - 1) + 1;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:ℝ| ((a < c) ∧ (c < b)) ∧ (Legendre(n;c) = r0)}  supposing (a\000C < b) ∧ ((Legendre(n;a) * Legendre(n;b)) < r0)
6. λi.rational_fun_zero(λx.ratLegendre(n;x);if i=0 then r(-1) else (z (i - 1));if i=n - 1 then r1 else (z i)) ∈ i:ℕn
   ⟶ {x:ℝ| 
       ((if i=0 then r(-1) else (z (i - 1)) < x) ∧ (x < if i=n - 1 then r1 else (z i)))
       ∧ (Legendre(n;x) = r0)
       ∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))} 
7. i : ℕn - 1
8. v : i:ℕn ⟶ {x:ℝ| 
                ((if i=0 then r(-1) else (z (i - 1)) < x) ∧ (x < if i=n - 1 then r1 else (z i)))
                ∧ (Legendre(n;x) = r0)
                ∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))} 
9. v1 : ℝ
10. (if i=0 then r(-1) else (z (i - 1)) < v1) ∧ (v1 < if i=n - 1 then r1 else (z i))
11. Legendre(n;v1) = r0
12. r0 < (r((-1)^(n - i)) * Legendre(n + 1;v1))
13. v2 : ℝ
14. (if i + 1=0 then r(-1) else (z ((i + 1) - 1)) < v2) ∧ (v2 < if i + 1=n - 1 then r1 else (z (i + 1)))
15. Legendre(n;v2) = r0
16. r0 < (r((-1)^(n - i + 1)) * Legendre(n + 1;v2))
⊢ v1 < v2
BY
{ ((Assert ¬((i + 1) = 0 ∈ ℤ) BY
          (All Thin THEN Auto))
   THEN (Assert ¬(i = (n - 1) ∈ ℤ) BY
               (All Thin THEN Auto))
   THEN ExRepD) }

1
1. n : ℤ
2. z : i:ℕn - 1 ⟶ {x:ℝ| 
                    ((r(-1) < x) ∧ (x < r1))
                    ∧ (Legendre(n - 1;x) = r0)
                    ∧ (r0 < (r((-1)^(n - 1 - i)) * Legendre((n - 1) + 1;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:ℝ| ((a < c) ∧ (c < b)) ∧ (Legendre(n;c) = r0)}  supposing (a\000C < b) ∧ ((Legendre(n;a) * Legendre(n;b)) < r0)
6. λi.rational_fun_zero(λx.ratLegendre(n;x);if i=0 then r(-1) else (z (i - 1));if i=n - 1 then r1 else (z i)) ∈ i:ℕn
   ⟶ {x:ℝ| 
       ((if i=0 then r(-1) else (z (i - 1)) < x) ∧ (x < if i=n - 1 then r1 else (z i)))
       ∧ (Legendre(n;x) = r0)
       ∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))} 
7. i : ℕn - 1
8. v : i:ℕn ⟶ {x:ℝ| 
                ((if i=0 then r(-1) else (z (i - 1)) < x) ∧ (x < if i=n - 1 then r1 else (z i)))
                ∧ (Legendre(n;x) = r0)
                ∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))} 
9. v1 : ℝ
10. if i=0 then r(-1) else (z (i - 1)) < v1
11. v1 < if i=n - 1 then r1 else (z i)
12. Legendre(n;v1) = r0
13. r0 < (r((-1)^(n - i)) * Legendre(n + 1;v1))
14. v2 : ℝ
15. if i + 1=0 then r(-1) else (z ((i + 1) - 1)) < v2
16. v2 < if i + 1=n - 1 then r1 else (z (i + 1))
17. Legendre(n;v2) = r0
18. r0 < (r((-1)^(n - i + 1)) * Legendre(n + 1;v2))
19. ¬((i + 1) = 0 ∈ ℤ)
20. ¬(i = (n - 1) ∈ ℤ)
⊢ v1 < v2

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  z  :  i:\mBbbN{}n  -  1  {}\mrightarrow{}  \{x:\mBbbR{}| 
                                        ((r(-1)  <  x)  \mwedge{}  (x  <  r1))
                                        \mwedge{}  (Legendre(n  -  1;x)  =  r0)
                                        \mwedge{}  (r0  <  (r((-1)\^{}(n  -  1  -  i))  *  Legendre((n  -  1)  +  1;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{}|  ((a  <  c)  \mwedge{}  (c  <  b))  \mwedge{}  (Legendre(n;c)  =  r0)\}  \000C 
          supposing  (a  <  b)  \mwedge{}  ((Legendre(n;a)  *  Legendre(n;b))  <  r0)
6.  \mlambda{}i.rational\_fun\_zero(\mlambda{}x.ratLegendre(n;x);if  i=0  then  r(-1)  else  (z  (i  -  1));if  i=n  -  1
                                                                                                                                                              then  r1
                                                                                                                                                              else  (z  i))  \mmember{}  i:\mBbbN{}n
      {}\mrightarrow{}  \{x:\mBbbR{}| 
              ((if  i=0  then  r(-1)  else  (z  (i  -  1))  <  x)  \mwedge{}  (x  <  if  i=n  -  1  then  r1  else  (z  i)))
              \mwedge{}  (Legendre(n;x)  =  r0)
              \mwedge{}  (r0  <  (r((-1)\^{}(n  -  i))  *  Legendre(n  +  1;x)))\} 
7.  i  :  \mBbbN{}n  -  1
8.  v  :  i:\mBbbN{}n  {}\mrightarrow{}  \{x:\mBbbR{}| 
                                ((if  i=0  then  r(-1)  else  (z  (i  -  1))  <  x)  \mwedge{}  (x  <  if  i=n  -  1  then  r1  else  (z  i)))
                                \mwedge{}  (Legendre(n;x)  =  r0)
                                \mwedge{}  (r0  <  (r((-1)\^{}(n  -  i))  *  Legendre(n  +  1;x)))\} 
9.  v1  :  \mBbbR{}
10.  (if  i=0  then  r(-1)  else  (z  (i  -  1))  <  v1)  \mwedge{}  (v1  <  if  i=n  -  1  then  r1  else  (z  i))
11.  Legendre(n;v1)  =  r0
12.  r0  <  (r((-1)\^{}(n  -  i))  *  Legendre(n  +  1;v1))
13.  v2  :  \mBbbR{}
14.  (if  i  +  1=0  then  r(-1)  else  (z  ((i  +  1)  -  1))  <  v2)
\mwedge{}  (v2  <  if  i  +  1=n  -  1  then  r1  else  (z  (i  +  1)))
15.  Legendre(n;v2)  =  r0
16.  r0  <  (r((-1)\^{}(n  -  i  +  1))  *  Legendre(n  +  1;v2))
\mvdash{}  v1  <  v2


By

---

Latex:
((Assert  \mneg{}((i  +  1)  =  0)  BY
                (All  Thin  THEN  Auto))
  THEN  (Assert  \mneg{}(i  =  (n  -  1))  BY
                          (All  Thin  THEN  Auto))
  THEN  ExRepD)

---

Home Index