---

Step * of Lemma BB-problem-21

∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀f,g:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} .
  ((∀x:ℝ. ((x ∈ [a, b]) ⇒ (r0 ≤ g[x])))
  ⇒ (∀e:{e:ℝ| r0 < e} . ∃c:{x:ℝ| x ∈ [a, b]} . (|a_∫-b f[x] * g[x] dx - f[c] * a_∫-b g[x] dx| < e)))
BY
{ (Auto
   THEN (Assert rmin(a;b) = a BY
               EAuto 1)
   THEN (Assert rmax(a;b) = b BY
               EAuto 1)
   THEN (RWO "integral-is-Riemann" 0 THENA Auto)) }

1
1. a : ℝ
2. b : {b:ℝ| a ≤ b} 
3. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
4. g : {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
5. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (r0 ≤ g[x]))
6. e : {e:ℝ| r0 < e} 
7. rmin(a;b) = a
8. rmax(a;b) = b
⊢ ∃c:{x:ℝ| x ∈ [a, b]} . (|∫ f[x] * g[x] dx on [a, b] - f[c] * ∫ g[x] dx on [a, b]| < e)

---

Latex:

---

Latex:
\mforall{}a:\mBbbR{}.  \mforall{}b:\{b:\mBbbR{}|  a  \mleq{}  b\}  .  \mforall{}f,g:\{f:[a,  b]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[a,  b])\}  .
    ((\mforall{}x:\mBbbR{}.  ((x  \mmember{}  [a,  b])  {}\mRightarrow{}  (r0  \mleq{}  g[x])))
    {}\mRightarrow{}  (\mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .  \mexists{}c:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  (|a\_\mint{}\msupminus{}b  f[x]  *  g[x]  dx  -  f[c]  *  a\_\mint{}\msupminus{}b  g[x]  dx|  <  e))\000C)


By

---

Latex:
(Auto
  THEN  (Assert  rmin(a;b)  =  a  BY
                          EAuto  1)
  THEN  (Assert  rmax(a;b)  =  b  BY
                          EAuto  1)
  THEN  (RWO  "integral-is-Riemann"  0  THENA  Auto))

---

Home Index