---

Step * of Lemma IVT-rpolynomial2

∀n:ℕ. ∀a:ℕn + 1 ⟶ ℝ. ∀b,c,d:ℝ.
  ((b ≤ c) ⇒ ((Σi≤n. a_i * b^i) < d) ⇒ (d < (Σi≤n. a_i * c^i)) ⇒ (∃x:{x:ℝ| x ∈ [b, c]} . ((Σi≤n. a_i * x^i) = d)))
BY
{ Auto }

1
1. n : ℕ
2. a : ℕn + 1 ⟶ ℝ
3. b : ℝ
4. c : ℝ
5. d : ℝ
6. b ≤ c
7. (Σi≤n. a_i * b^i) < d
8. d < (Σi≤n. a_i * c^i)
⊢ ∃x:{x:ℝ| x ∈ [b, c]} . ((Σi≤n. a_i * x^i) = d)

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index