---

Step * 2 1 2 1 of Lemma sine-medium_wf

.....set predicate..... 
1. x : ℝ
2. r(-2) ≤ x
3. x ≤ r(2)
4. y : x < r1
5. x1 : (r(49))/100 < x
6. |(x)/2| ≤ (r1/r(2))
⊢ 2 * sine-small((x)/2) * cosine-small((x)/2) = sine(x)
BY
{ ((InstLemma `rsin-reduce2` [⌜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)/2)⌝;⌜sine-small((x)/2)⌝]⋅
   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.  y  :  x  <  r1
5.  x1  :  (r(49))/100  <  x
6.  |(x)/2|  \mleq{}  (r1/r(2))
\mvdash{}  2  *  sine-small((x)/2)  *  cosine-small((x)/2)  =  sine(x)


By

---

Latex:
((InstLemma  `rsin-reduce2`  [\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)/2)\mkleeneclose{};\mkleeneopen{}sine-small((x)/2)\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  DSetVars
  THEN  (Unhide  THENA  Auto)
  THEN  RWO    "-3  -1"  0
  THEN  Auto)

---

Home Index