---

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

∀n:ℕ. ∀a:ℕn + 1 ⟶ ℝ.
  (((Σi≤n. a_i * r0^i) < r0) ⇒ (r0 < (Σi≤n. a_i * r1^i)) ⇒ locally-non-constant(λx.(Σi≤n. a_i * x^i);r0;r1;r0))
BY
{ (Auto THEN BLemma `locally-non-constant-deriv-seq-test` THEN Auto) }

1
1. n : ℕ
2. a : ℕn + 1 ⟶ ℝ
3. (Σi≤n. a_i * r0^i) < r0
4. r0 < (Σi≤n. a_i * r1^i)
5. u : {u:ℝ| u ∈ [r0, r1]} 
6. v : {v:ℝ| v ∈ [r0, r1]} 
7. u < v
⊢ ∃k:ℕ
   ∃F:ℕk + 1 ⟶ [r0, r1] ⟶ℝ
    (finite-deriv-seq([r0, r1];k;i,x.F[i;x])
    ∧ (∀x:{x:ℝ| x ∈ [r0, r1]} . (F[0;x] = (λx.(Σi≤n. a_i * x^i)(x) - r0)))
    ∧ (∃z:{z:ℝ| z ∈ [u, v]} . (r0 < Σ{|F[i;z]| | 0≤i≤k})))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}.
    (((\mSigma{}i\mleq{}n.  a\_i  *  r0\^{}i)  <  r0)
    {}\mRightarrow{}  (r0  <  (\mSigma{}i\mleq{}n.  a\_i  *  r1\^{}i))
    {}\mRightarrow{}  locally-non-constant(\mlambda{}x.(\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i);r0;r1;r0))


By

---

Latex:
(Auto  THEN  BLemma  `locally-non-constant-deriv-seq-test`  THEN  Auto)

---

Home Index