---

Step * 1 of Lemma radd_rcos-deriv-seq


1. i : ℤ
2. i = 1 ∈ ℤ
⊢ d(r1 - rsin(x))/dx = λx.-(rcos(x)) on (-∞, ∞)
BY
{ ((AssertDerivative THENA ProveDerivative THENA Auto)
   THEN DerivativeFunctionality (-1)
   THEN Auto
   THEN nRNorm 0
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((AssertDerivative  THENA  ProveDerivative  THENA  Auto)
  THEN  DerivativeFunctionality  (-1)
  THEN  Auto
  THEN  nRNorm  0
  THEN  Auto)

---

Home Index