---

Step * 1 of Lemma derivative-const-mul2


1. a : ℝ@i
2. I : Interval@i
3. f : I ⟶ℝ@i
4. g : I ⟶ℝ@i
5. λx.g[x] = d(f[x])/dx on I@i
6. λx.a * g[x] = d(a * f[x])/dx on I
⊢ λx.g[x] * a = d(f[x] * a)/dx on I
BY
{ (DerivativeFunctionality (-1) THEN Auto THEN nRNorm 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}@i
2.  I  :  Interval@i
3.  f  :  I  {}\mrightarrow{}\mBbbR{}@i
4.  g  :  I  {}\mrightarrow{}\mBbbR{}@i
5.  \mlambda{}x.g[x]  =  d(f[x])/dx  on  I@i
6.  \mlambda{}x.a  *  g[x]  =  d(a  *  f[x])/dx  on  I
\mvdash{}  \mlambda{}x.g[x]  *  a  =  d(f[x]  *  a)/dx  on  I


By

---

Latex:
(DerivativeFunctionality  (-1)  THEN  Auto  THEN  nRNorm  0  THEN  Auto)

---

Home Index