---

Step * 2 2 2 1 1 of Lemma sine-medium_wf


1. x : ℝ
2. r(-2) ≤ x
3. x ≤ r(2)
4. y : x < r1
5. y1 : x < (r1)/2
6. y2 : x < (r(-49))/100
7. x1 : r(-1) < x
8. |(x)/2| < (r1)/2
⊢ 2 * sine-small((x)/2) * cosine-small((x)/2) ∈ {y:ℝ| y = sine(x)} 
BY
{ ((Assert (x)/2 ∈ {x:ℝ| |x| ≤ (r1/r(2))}  BY
          (MemTypeCD THEN Auto THEN RWO "int-rdiv-req<" 0 THEN Auto))
   THEN (InstLemma `rsin-reduce2` [⌜x⌝]⋅ THENA Auto)
   THEN (RWW "rsin-is-sine rcos-is-cosine" (-1) THENA Auto)
   THEN MemTypeCD
   THEN 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:

1.  x  :  \mBbbR{}
2.  r(-2)  \mleq{}  x
3.  x  \mleq{}  r(2)
4.  y  :  x  <  r1
5.  y1  :  x  <  (r1)/2
6.  y2  :  x  <  (r(-49))/100
7.  x1  :  r(-1)  <  x
8.  |(x)/2|  <  (r1)/2
\mvdash{}  2  *  sine-small((x)/2)  *  cosine-small((x)/2)  \mmember{}  \{y:\mBbbR{}|  y  =  sine(x)\} 


By

---

Latex:
((Assert  (x)/2  \mmember{}  \{x:\mBbbR{}|  |x|  \mleq{}  (r1/r(2))\}    BY
                (MemTypeCD  THEN  Auto  THEN  RWO  "int-rdiv-req<"  0  THEN  Auto))
  THEN  (InstLemma  `rsin-reduce2`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWW  "rsin-is-sine  rcos-is-cosine"  (-1)  THENA  Auto)
  THEN  MemTypeCD
  THEN  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