---

Step * 1 1 of Lemma sine-cosine-pythag

.....antecedent..... 
1. x : ℝ
⊢ d((sine(x) * sine(x)) + (cosine(x) * cosine(x)))/dx = λx.r0 on (-∞, ∞)
BY
{ ((AssertDerivative THENA (ProveDerivative THEN Auto THEN MemTypeCD THEN Reduce 0 THEN Auto))
   THEN DerivativeFunctionality (-1)
   THEN Auto
   THEN nRNorm 0
   THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  x  :  \mBbbR{}
\mvdash{}  d((sine(x)  *  sine(x))  +  (cosine(x)  *  cosine(x)))/dx  =  \mlambda{}x.r0  on  (-\minfty{},  \minfty{})


By

---

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

---

Home Index