---

Step * 1 of Lemma sine-cosine-pythag


1. x : ℝ
⊢ (sine(x)^2 + cosine(x)^2) = r1
BY
{ ((RWO "rnexp2" 0 THENA Auto)
   THEN (InstLemma `derivative-is-zero` [⌜(-∞, ∞)⌝;⌜λ2x.(sine(x) * sine(x)) + (cosine(x) * cosine(x))⌝]⋅ THENA Auto)
   THEN D -1
   THEN Thin
   (-1)⋅
   THEN D -1) }

1
.....antecedent..... 
1. x : ℝ
⊢ d((sine(x) * sine(x)) + (cosine(x) * cosine(x)))/dx = λx.r0 on (-∞, ∞)

2
1. x : ℝ
2. ∃c:ℝ. ∀x:{x:ℝ| x ∈ (-∞, ∞)} . (((sine(x) * sine(x)) + (cosine(x) * cosine(x))) = c)
⊢ ((sine(x) * sine(x)) + (cosine(x) * cosine(x))) = r1

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
\mvdash{}  (sine(x)\^{}2  +  cosine(x)\^{}2)  =  r1


By

---

Latex:
((RWO  "rnexp2"  0  THENA  Auto)
  THEN  (InstLemma  `derivative-is-zero`  [\mkleeneopen{}(-\minfty{},  \minfty{})\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.(sine(x)  *  sine(x))  +  (cosine(x)  *  cosine(x))\mkleeneclose{}
              ]\mcdot{}
              THENA  Auto
              )
  THEN  D  -1
  THEN  Thin
  (-1)\mcdot{}
  THEN  D  -1)

---

Home Index