---

Step * of Lemma integration-by-parts

∀I:Interval. ∀u,v,h:I ⟶ℝ. ∀u',v':{h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))} .
  (d(u[t])/dt = λt.u'[t] on I
  ⇒ d(v[t])/dt = λt.v'[t] on I
  ⇒ d(h[t])/dt = λt.u'[t] * v[t] on I
  ⇒ d((u[t] * v[t]) - h[t])/dt = λt.u[t] * v'[t] on I)
BY
{ (Auto
   THEN (Assert d((u[t] * v[t]) - h[t])/dt = λt.((u[t] * v'[t]) + (v[t] * u'[t])) - u'[t] * v[t] on I BY
               (ProveDerivative THEN DSetVars THEN Auto))
   THEN DerivativeFunctionality (-1)
   THEN Auto
   THEN nRNorm 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}u,v,h:I  {}\mrightarrow{}\mBbbR{}.  \mforall{}u',v':\{h:I  {}\mrightarrow{}\mBbbR{}|  \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  ((h  x)  =  (h  y)))\}  .
    (d(u[t])/dt  =  \mlambda{}t.u'[t]  on  I
    {}\mRightarrow{}  d(v[t])/dt  =  \mlambda{}t.v'[t]  on  I
    {}\mRightarrow{}  d(h[t])/dt  =  \mlambda{}t.u'[t]  *  v[t]  on  I
    {}\mRightarrow{}  d((u[t]  *  v[t])  -  h[t])/dt  =  \mlambda{}t.u[t]  *  v'[t]  on  I)


By

---

Latex:
(Auto
  THEN  (Assert  d((u[t]  *  v[t])  -  h[t])/dt  =  \mlambda{}t.((u[t]  *  v'[t])  +  (v[t]  *  u'[t]))  -  u'[t]
                          *  v[t]  on  I  BY
                          (ProveDerivative  THEN  DSetVars  THEN  Auto))
  THEN  DerivativeFunctionality  (-1)
  THEN  Auto
  THEN  nRNorm  0
  THEN  Auto)

---

Home Index