---

Step * of Lemma rsin-rminus

∀x:ℝ. (rsin(-(x)) = -(rsin(x)))
BY
{ (Auto THEN (InstLemma `derivative_unique` [⌜(-∞, ∞)⌝;⌜λ2x.rcos(x)⌝;⌜λ2x.-(rsin(x))⌝;⌜λ2x.rsin(-(x))⌝]⋅ THENA Auto)) }

1
.....antecedent..... 
1. x : ℝ
⊢ d(rcos(x))/dx = λx.rsin(-(x)) on (-∞, ∞)

2
1. x : ℝ
2. rfun-eq((-∞, ∞);λ2x.-(rsin(x));λ2x.rsin(-(x)))
⊢ rsin(-(x)) = -(rsin(x))

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  (rsin(-(x))  =  -(rsin(x)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `derivative\_unique`  [\mkleeneopen{}(-\minfty{},  \minfty{})\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rcos(x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.-(rsin(x))\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rsin(-(x))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  )

---

Home Index