---

Step * 1 1 1 2 1 2 1 1 2 1 2 2 1 1 1 1 1 2 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. rpoly-nth-deriv(i;n - 1;a;u) = rpoly-nth-deriv(i;n;λk.if (k =z n) then r0 else a k fi ;u)
⊢ rpoly-nth-deriv(i;n;a;u)
= rpoly-nth-deriv(i;n;λi.(((λk.if (k =z n) then a n else r0 fi ) i) + ((λk.if (k =z n) then r0 else a k fi ) i));u)
BY
{ TACTIC:Reduce 0 }

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. rpoly-nth-deriv(i;n - 1;a;u) = rpoly-nth-deriv(i;n;λk.if (k =z n) then r0 else a k fi ;u)
⊢ rpoly-nth-deriv(i;n;a;u)
= rpoly-nth-deriv(i;n;λi.(if (i =z n) then a n else r0 fi  + if (i =z n) then r0 else a i fi );u)

---

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.  rpoly-nth-deriv(i;n  -  1;a;u)  =  rpoly-nth-deriv(i;n;\mlambda{}k.if  (k  =\msubz{}  n)  then  r0  else  a  k  fi  ;u)
\mvdash{}  rpoly-nth-deriv(i;n;a;u)
=  rpoly-nth-deriv(i;n;\mlambda{}i.(((\mlambda{}k.if  (k  =\msubz{}  n)  then  a  n  else  r0  fi  )  i)
                                                  +  ((\mlambda{}k.if  (k  =\msubz{}  n)  then  r0  else  a  k  fi  )  i));u)


By

---

Latex:
TACTIC:Reduce  0

---

Home Index