---

Step * of Lemma intermediate-value-theorem-rpolynomial

∀n:ℕ. ∀a:ℕn + 1 ⟶ ℝ. ∀b,c,d:ℝ.
  (∃x:{x:ℝ| x ∈ [b, c]} . ((Σi≤n. a_i * x^i) = d)) supposing 
     ((d < (Σi≤n. a_i * c^i)) and 
     ((Σi≤n. a_i * b^i) < d) and 
     (b ≤ c))
BY
{ (Auto THEN BLemma `IVT-rpolynomial2` THEN Auto THEN Unhide THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}.  \mforall{}b,c,d:\mBbbR{}.
    (\mexists{}x:\{x:\mBbbR{}|  x  \mmember{}  [b,  c]\}  .  ((\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)  =  d))  supposing 
          ((d  <  (\mSigma{}i\mleq{}n.  a\_i  *  c\^{}i))  and 
          ((\mSigma{}i\mleq{}n.  a\_i  *  b\^{}i)  <  d)  and 
          (b  \mleq{}  c))


By

---

Latex:
(Auto  THEN  BLemma  `IVT-rpolynomial2`  THEN  Auto  THEN  Unhide  THEN  Auto)

---

Home Index