---

Step * of Lemma Legendre-roots-lemma2

∀n:ℕ. ∀z:ℕn - 1 ⟶ {x:ℝ| x ∈ (r(-1), r1)} .
  ((∀i:ℕn - 1. (Legendre(n - 1;z i) = r0))
  ⇒ (∀i:ℕn - 2. ((z i) < (z (i + 1))))
  ⇒ (∀i:ℕn. ∀v:{v:ℝ| (v ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i))) ∧ (Legendre(n;v) = r0)} \000C.
        (r0 < (r(-1)^n - i * Legendre(n + 1;v)))))
BY
{ ((D 0 THENA Auto)
   THEN (CaseNat 0 `n'
         THENL [Auto
               ; (CaseNat 1 `n'
                  THENL [(HypSubst' (-1) 0
                          THEN Reduce 0
                          THEN Auto
                          THEN IntSegCases (-2)
                          THEN HypSubst' (-1) (-2)
                          THEN ThinVar `i'
                          THEN All Reduce)
                        ; (InstLemma `Legendre-roots-lemma` [⌜n⌝]⋅ THEN Auto)]
               )]
        )
   ) }

1
1. n : ℕ
2. ¬(n = 0 ∈ ℤ)
3. n = 1 ∈ ℤ
4. z@0 : ℕ0 ⟶ {x:ℝ| (r(-1) < x) ∧ (x < r1)} 
5. ∀i:ℕ0. (r1 = r0)
6. ∀i:ℕ-1. ((z@0 i) < (z@0 (i + 1)))
7. v : {v:ℝ| ((r(-1) < v) ∧ (v < r1)) ∧ (v = r0)} 
⊢ r0 < (r(-1)^1 * Legendre(2;v))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}z:\mBbbN{}n  -  1  {}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  (r(-1),  r1)\}  .
    ((\mforall{}i:\mBbbN{}n  -  1.  (Legendre(n  -  1;z  i)  =  r0))
    {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n  -  2.  ((z  i)  <  (z  (i  +  1))))
    {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n.  \mforall{}v:\{v:\mBbbR{}| 
                                  (v  \mmember{}  (if  i=0  then  r(-1)  else  (z  (i  -  1)),  if  i=n  -  1  then  r1  else  (z  i)))
                                  \mwedge{}  (Legendre(n;v)  =  r0)\}  .
                (r0  <  (r(-1)\^{}n  -  i  *  Legendre(n  +  1;v)))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (CaseNat  0  `n'
              THENL  [Auto
                          ;  (CaseNat  1  `n'
                                THENL  [(HypSubst'  (-1)  0
                                                THEN  Reduce  0
                                                THEN  Auto
                                                THEN  IntSegCases  (-2)
                                                THEN  HypSubst'  (-1)  (-2)
                                                THEN  ThinVar  `i'
                                                THEN  All  Reduce)
                                            ;  (InstLemma  `Legendre-roots-lemma`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)]
                          )]
            )
  )

---

Home Index