---

Step * 1 2 1 of Lemma sine-medium_wf

.....set predicate..... 
1. x : ℝ
2. r(-2) ≤ x
3. x ≤ r(2)
4. x1 : (r(99))/100 < x
5. |(x)/4| ≤ (r1/r(2))
⊢ 4 * cosine-small((x)/4) * (sine-small((x)/4) - 2 * sine-small((x)/4)^3) = sine(x)
BY
{ ((InstLemma `rsin-reduce4` [⌜x⌝]⋅ THENA Auto)
   THEN (RWW "rsin-is-sine rcos-is-cosine" (-1) THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN GenConclTerms Auto [⌜cosine-small((x)/4)⌝;⌜sine-small((x)/4)⌝]⋅
   THEN All Thin
   THEN DSetVars
   THEN (Unhide THENA Auto)
   THEN RWO  "-3 -1" 0
   THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  x  :  \mBbbR{}
2.  r(-2)  \mleq{}  x
3.  x  \mleq{}  r(2)
4.  x1  :  (r(99))/100  <  x
5.  |(x)/4|  \mleq{}  (r1/r(2))
\mvdash{}  4  *  cosine-small((x)/4)  *  (sine-small((x)/4)  -  2  *  sine-small((x)/4)\^{}3)  =  sine(x)


By

---

Latex:
((InstLemma  `rsin-reduce4`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWW  "rsin-is-sine  rcos-is-cosine"  (-1)  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}cosine-small((x)/4)\mkleeneclose{};\mkleeneopen{}sine-small((x)/4)\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  DSetVars
  THEN  (Unhide  THENA  Auto)
  THEN  RWO    "-3  -1"  0
  THEN  Auto)

---

Home Index