---

Step * of Lemma radd_rcos-deriv-seq

finite-deriv-seq((-∞, ∞);3;i,x.if (i =z 0) then radd_rcos(x)
if (i =z 1) then r1 - rsin(x)
if (i =z 2) then -(rcos(x))
else rsin(x)
fi )
BY
{ ((D 0 THENA Auto) THEN IntSegCases 1 THEN Reduce 0 THEN Auto THEN ProveDerivative THEN Auto) }

1
1. i : ℤ
2. i = 1 ∈ ℤ
⊢ d(r1 - rsin(x))/dx = λx.-(rcos(x)) on (-∞, ∞)

---

Latex:

---

Latex:
finite-deriv-seq((-\minfty{},  \minfty{});3;i,x.if  (i  =\msubz{}  0)  then  radd\_rcos(x)
if  (i  =\msubz{}  1)  then  r1  -  rsin(x)
if  (i  =\msubz{}  2)  then  -(rcos(x))
else  rsin(x)
fi  )


By

---

Latex:
((D  0  THENA  Auto)  THEN  IntSegCases  1  THEN  Reduce  0  THEN  Auto  THEN  ProveDerivative  THEN  Auto)

---

Home Index