---

Step * 1 1 1 1 1 1 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. ∀i,j:ℕn - 1.  (i < j ⇒ ((z i) < (z j)))
9. ∀i,j:ℕn - 1.  ((i ≤ j) ⇒ ((z i) ≤ (z j)))
10. rprod(0;n - 2;k.v - z k) = (rprod(0;i - 1;k.v - z k) * rprod((i - 1) + 1;n - 2;k.v - z k))
⊢ r0 < -(r(-1)^n - i * rprod(0;n - 2;j.v - z j))
BY
{ ((Subst' (i - 1) + 1 ~ i -1 THENA Auto)
   THEN (Assert r0 < rprod(0;i - 1;k.v - z k) BY
               (BLemma `rprod-of-positive`
                THEN Auto
                THEN (Subst' (i - 1) + 1 ~ i -1 THENA Auto)
                THEN (CaseNat 0 `i'
                      THENL [Auto
                            ; ((Reduce -6 THENA Auto)
                               THEN nRAdd ⌜z k⌝ 0⋅
                               THEN (Assert (z k) ≤ (z (i - 1)) BY
                                           (BHyp -4 THEN Auto))
                               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. ∀i,j:ℕn - 1.  (i < j ⇒ ((z i) < (z j)))
9. ∀i,j:ℕn - 1.  ((i ≤ j) ⇒ ((z i) ≤ (z j)))
10. rprod(0;n - 2;k.v - z k) = (rprod(0;i - 1;k.v - z k) * rprod(i;n - 2;k.v - z k))
11. r0 < rprod(0;i - 1;k.v - z k)
⊢ r0 < -(r(-1)^n - i * rprod(0;n - 2;j.v - z j))

---

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.  \mforall{}i,j:\mBbbN{}n  -  1.    (i  <  j  {}\mRightarrow{}  ((z  i)  <  (z  j)))
9.  \mforall{}i,j:\mBbbN{}n  -  1.    ((i  \mleq{}  j)  {}\mRightarrow{}  ((z  i)  \mleq{}  (z  j)))
10.  rprod(0;n  -  2;k.v  -  z  k)  =  (rprod(0;i  -  1;k.v  -  z  k)  *  rprod((i  -  1)  +  1;n  -  2;k.v  -  z  k))
\mvdash{}  r0  <  -(r(-1)\^{}n  -  i  *  rprod(0;n  -  2;j.v  -  z  j))


By

---

Latex:
((Subst'  (i  -  1)  +  1  \msim{}  i  -1  THENA  Auto)
  THEN  (Assert  r0  <  rprod(0;i  -  1;k.v  -  z  k)  BY
                          (BLemma  `rprod-of-positive`
                            THEN  Auto
                            THEN  (Subst'  (i  -  1)  +  1  \msim{}  i  -1  THENA  Auto)
                            THEN  (CaseNat  0  `i'
                                        THENL  [Auto
                                                    ;  ((Reduce  -6  THENA  Auto)
                                                          THEN  nRAdd  \mkleeneopen{}z  k\mkleeneclose{}  0\mcdot{}
                                                          THEN  (Assert  (z  k)  \mleq{}  (z  (i  -  1))  BY
                                                                                  (BHyp  -4  THEN  Auto))
                                                          THEN  Auto)]
                            )))
  )

---

Home Index