---

Step * 1 2 of Lemma rsin-rminus


1. x : ℝ
2. d(rcos(-(x)))/dx = λx.rsin(-(x)) on (-∞, ∞)
⊢ d(rcos(x))/dx = λx.rsin(-(x)) on (-∞, ∞)
BY
{ (InstLemma `derivative_functionality` [⌜(-∞, ∞)⌝;⌜λ2x.rcos(-(x))⌝;⌜λ2x.rcos(x)⌝;⌜λ2x.rsin(-(x))⌝;⌜λ2x.rsin(-(x))⌝]⋅
   THEN Auto
   THEN RepUR ``rfun-eq r-ap so_lambda`` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  d(rcos(-(x)))/dx  =  \mlambda{}x.rsin(-(x))  on  (-\minfty{},  \minfty{})
\mvdash{}  d(rcos(x))/dx  =  \mlambda{}x.rsin(-(x))  on  (-\minfty{},  \minfty{})


By

---

Latex:
(InstLemma  `derivative\_functionality`  [\mkleeneopen{}(-\minfty{},  \minfty{})\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rcos(-(x))\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rcos(x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rsin(-(x))\mkleeneclose{};
  \mkleeneopen{}\mlambda{}\msubtwo{}x.rsin(-(x))\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  RepUR  ``rfun-eq  r-ap  so\_lambda``  0
  THEN  Auto)

---

Home Index