---

Step * 1 1 1 2 1 2 1 1 2 1 2 2 1 1 1 1 1 1 1 of Lemma rpolynomial-locally-non-zero-1


1. n : ℤ
2. 0 < n
3. ∀a:ℕ(n - 1) + 1 ⟶ ℝ
     ((r0 < Σ{a i | 0≤i≤n - 1})
     ⇒ ((a 0) < r0)
     ⇒ (∀u:{u:ℝ| u ∈ [r0, r1]} . (r0 < Σ{|rpoly-nth-deriv(i;n - 1;a;u)| | 0≤i≤n - 1})))
4. a : ℕn + 1 ⟶ ℝ
5. r0 < (Σ{a i | 0≤i≤n - 1} + (a n))
6. (a 0) < r0
7. u : {u:ℝ| u ∈ [r0, r1]} 
8. (r0 < |a n|) ⇒ (r0 < Σ{|rpoly-nth-deriv(i;n;a;u)| | 0≤i≤n})
9. r0 < Σ{a i | 0≤i≤n - 1}
10. r0 < Σ{|rpoly-nth-deriv(i;n - 1;a;u)| | 0≤i≤n - 1}
11. i : ℤ
12. 0 ≤ i
13. i ≤ n
14. n - 1 < i
⊢ r0 = (Σi≤n - i. poly-nth-deriv(i;λk.if (k =z n) then r0 else a k fi )_i * u^i)
BY
{ ((Subst' i ~ n 0 THENA Auto') THEN (Subst' n - n ~ 0 0 THENA Auto)) }

1
1. n : ℤ
2. 0 < n
3. ∀a:ℕ(n - 1) + 1 ⟶ ℝ
     ((r0 < Σ{a i | 0≤i≤n - 1})
     ⇒ ((a 0) < r0)
     ⇒ (∀u:{u:ℝ| u ∈ [r0, r1]} . (r0 < Σ{|rpoly-nth-deriv(i;n - 1;a;u)| | 0≤i≤n - 1})))
4. a : ℕn + 1 ⟶ ℝ
5. r0 < (Σ{a i | 0≤i≤n - 1} + (a n))
6. (a 0) < r0
7. u : {u:ℝ| u ∈ [r0, r1]} 
8. (r0 < |a n|) ⇒ (r0 < Σ{|rpoly-nth-deriv(i;n;a;u)| | 0≤i≤n})
9. r0 < Σ{a i | 0≤i≤n - 1}
10. r0 < Σ{|rpoly-nth-deriv(i;n - 1;a;u)| | 0≤i≤n - 1}
11. i : ℤ
12. 0 ≤ i
13. i ≤ n
14. n - 1 < i
⊢ r0 = (Σi≤0. poly-nth-deriv(n;λk.if (k =z n) then r0 else a k fi )_i * u^i)

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}a:\mBbbN{}(n  -  1)  +  1  {}\mrightarrow{}  \mBbbR{}
          ((r0  <  \mSigma{}\{a  i  |  0\mleq{}i\mleq{}n  -  1\})
          {}\mRightarrow{}  ((a  0)  <  r0)
          {}\mRightarrow{}  (\mforall{}u:\{u:\mBbbR{}|  u  \mmember{}  [r0,  r1]\}  .  (r0  <  \mSigma{}\{|rpoly-nth-deriv(i;n  -  1;a;u)|  |  0\mleq{}i\mleq{}n  -  1\})))
4.  a  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}
5.  r0  <  (\mSigma{}\{a  i  |  0\mleq{}i\mleq{}n  -  1\}  +  (a  n))
6.  (a  0)  <  r0
7.  u  :  \{u:\mBbbR{}|  u  \mmember{}  [r0,  r1]\} 
8.  (r0  <  |a  n|)  {}\mRightarrow{}  (r0  <  \mSigma{}\{|rpoly-nth-deriv(i;n;a;u)|  |  0\mleq{}i\mleq{}n\})
9.  r0  <  \mSigma{}\{a  i  |  0\mleq{}i\mleq{}n  -  1\}
10.  r0  <  \mSigma{}\{|rpoly-nth-deriv(i;n  -  1;a;u)|  |  0\mleq{}i\mleq{}n  -  1\}
11.  i  :  \mBbbZ{}
12.  0  \mleq{}  i
13.  i  \mleq{}  n
14.  n  -  1  <  i
\mvdash{}  r0  =  (\mSigma{}i\mleq{}n  -  i.  poly-nth-deriv(i;\mlambda{}k.if  (k  =\msubz{}  n)  then  r0  else  a  k  fi  )\_i  *  u\^{}i)


By

---

Latex:
((Subst'  i  \msim{}  n  0  THENA  Auto')  THEN  (Subst'  n  -  n  \msim{}  0  0  THENA  Auto))

---

Home Index