---

Step * of Lemma ftc-total-integral

∀f,g:ℝ ⟶ ℝ.
  ((∀x,y:ℝ.  ((x = y) ⇒ (f[x] = f[y])))
  ⇒ d(g[x])/dx = λx.f[x] on (-∞, ∞)
  ⇒ (∀a,b:ℝ.  (a_∫-b f[t] dt = (g[b] - g[a]))))
BY
{ (Auto
   THEN (InstLemma `ftc-integral` [⌜(-∞, ∞)⌝;⌜a⌝;⌜b⌝;⌜f⌝;⌜g⌝]⋅ THENA (Auto THEN RepUR ``iproper i-finite`` 0 THEN Auto))
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}f,g:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}.
    ((\mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y])))
    {}\mRightarrow{}  d(g[x])/dx  =  \mlambda{}x.f[x]  on  (-\minfty{},  \minfty{})
    {}\mRightarrow{}  (\mforall{}a,b:\mBbbR{}.    (a\_\mint{}\msupminus{}b  f[t]  dt  =  (g[b]  -  g[a]))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `ftc-integral`  [\mkleeneopen{}(-\minfty{},  \minfty{})\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  RepUR  ``iproper  i-finite``  0  THEN  Auto)
              )
  THEN  Trivial)

---

Home Index