---

Step * of Lemma rpolynomial-locally-non-zero

∀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 D 0 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 : ℝ
6. v : ℝ
7. r0 ≤ u
8. u < v
9. v ≤ r1
⊢ ∃z:ℝ. ((u ≤ z) ∧ (z ≤ v) ∧ λx.(Σi≤n. a_i * x^i)(z) ≠ r0)

---

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  D  0  THEN  Auto)

---

Home Index