---

Step * 1 of Lemma derivative-mul-x


1. I : Interval
2. f : I ⟶ℝ
3. g : {h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))} 
4. d(f[x])/dx = λx.g[x] on I
⊢ d(x * f[x])/dx = λx.(x * g[x]) + f[x] on I
BY
{ (Assert d(x * f[x])/dx = λx.(x * g[x]) + (f[x] * r1) on I BY
         (ProveDerivative THEN Auto THEN DVar `g' THEN Unhide THEN Auto)) }

1
1. I : Interval
2. f : I ⟶ℝ
3. g : {h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((h x) = (h y)))} 
4. d(f[x])/dx = λx.g[x] on I
5. d(x * f[x])/dx = λx.(x * g[x]) + (f[x] * r1) on I
⊢ d(x * f[x])/dx = λx.(x * g[x]) + f[x] on I

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  g  :  \{h:I  {}\mrightarrow{}\mBbbR{}|  \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  ((h  x)  =  (h  y)))\} 
4.  d(f[x])/dx  =  \mlambda{}x.g[x]  on  I
\mvdash{}  d(x  *  f[x])/dx  =  \mlambda{}x.(x  *  g[x])  +  f[x]  on  I


By

---

Latex:
(Assert  d(x  *  f[x])/dx  =  \mlambda{}x.(x  *  g[x])  +  (f[x]  *  r1)  on  I  BY
              (ProveDerivative  THEN  Auto  THEN  DVar  `g'  THEN  Unhide  THEN  Auto))

---

Home Index