Step
*
of Lemma
derivative-rcos
d(rcos(x))/dx = λx.-(rsin(x)) on (-∞, ∞)
BY
{ ((Assert d(cosine(x))/dx = λx.-(sine(x)) on (-∞, ∞) BY
          Auto)
   THEN DerivativeFunctionality (-1)
   THEN Auto
   THEN RWO "rsin-is-sine rcos-is-cosine" 0
   THEN Auto) }
Latex:
Latex:
d(rcos(x))/dx  =  \mlambda{}x.-(rsin(x))  on  (-\minfty{},  \minfty{})
By
Latex:
((Assert  d(cosine(x))/dx  =  \mlambda{}x.-(sine(x))  on  (-\minfty{},  \minfty{})  BY
                Auto)
  THEN  DerivativeFunctionality  (-1)
  THEN  Auto
  THEN  RWO  "rsin-is-sine  rcos-is-cosine"  0
  THEN  Auto)
Home
Index