---

Step * of Lemma derivative-add-const

∀[I:Interval]. ∀[C:ℝ]. ∀[f,g:I ⟶ℝ].  (d(f[x])/dx = λx.g[x] on I ⇒ d(C + f[x])/dx = λx.g[x] on I)
BY
{ xxx(Auto
      THEN (Assert d(C + f[x])/dx = λx.r0 + g[x] on I BY
                  (ProveDerivative THEN Auto))
      THEN DerivativeFunctionality (-1)
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[I:Interval].  \mforall{}[C:\mBbbR{}].  \mforall{}[f,g:I  {}\mrightarrow{}\mBbbR{}].    (d(f[x])/dx  =  \mlambda{}x.g[x]  on  I  {}\mRightarrow{}  d(C  +  f[x])/dx  =  \mlambda{}x.g[x]  on  I)


By

---

Latex:
xxx(Auto
        THEN  (Assert  d(C  +  f[x])/dx  =  \mlambda{}x.r0  +  g[x]  on  I  BY
                                (ProveDerivative  THEN  Auto))
        THEN  DerivativeFunctionality  (-1)
        THEN  Auto)xxx

---

Home Index