---

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


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 - 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:ℝ| (c ∈ (a, b)) ∧ (Legendre(n;c) = r0)}  supposing (a < b) ∧\000C ((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:ℝ| 
       (x ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i)))
       ∧ (Legendre(n;x) = r0)
       ∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))} 
⊢ ∃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
{ D 0 With ⌜λ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))⌝  }

1
.....wf..... 
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 - 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:ℝ| (c ∈ (a, b)) ∧ (Legendre(n;c) = r0)}  supposing (a < b) ∧\000C ((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:ℝ| 
       (x ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i)))
       ∧ (Legendre(n;x) = r0)
       ∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))} 
⊢ λ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:ℝ| (x ∈ (r(-1), r1)) ∧ (Legendre(n;x) = r0) ∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))} 

2
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 - 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:ℝ| (c ∈ (a, b)) ∧ (Legendre(n;c) = r0)}  supposing (a < b) ∧\000C ((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:ℝ| 
       (x ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i)))
       ∧ (Legendre(n;x) = r0)
       ∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))} 
⊢ ∀i:ℕn - 1
    (((λ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) < ((λ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 + 1)))

3
.....wf..... 
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 - 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:ℝ| (c ∈ (a, b)) ∧ (Legendre(n;c) = r0)}  supposing (a < b) ∧\000C ((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:ℝ| 
       (x ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i)))
       ∧ (Legendre(n;x) = r0)
       ∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))} 
7. z1 : i:ℕn ⟶ {x:ℝ| (x ∈ (r(-1), r1)) ∧ (Legendre(n;x) = r0) ∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))} 
⊢ istype(∀i:ℕn - 1. ((z1 i) < (z1 (i + 1))))

---

Latex:

---

Latex:

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  -  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{}|  (c  \mmember{}  (a,  b))  \mwedge{}  (Legendre(n;c)  =  r0)\}   
          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{}| 
              (x  \mmember{}  (if  i=0  then  r(-1)  else  (z  (i  -  1)),  if  i=n  -  1  then  r1  else  (z  i)))
              \mwedge{}  (Legendre(n;x)  =  r0)
              \mwedge{}  (r0  <  (r((-1)\^{}(n  -  i))  *  Legendre(n  +  1;x)))\} 
\mvdash{}  \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))))]


By

---

Latex:
D  0  With  \mkleeneopen{}\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))\mkleeneclose{} 

---

Home Index