---

Step * 2 2 1 1 of Lemma cosine-medium_wf


1. x : ℝ
2. r(-2) ≤ x
3. x ≤ r(2)
4. y : x < r1
5. y1 : x < (r1)/2
6. x1 : (r(-1))/2 < x
7. |x| < (r1)/2
⊢ cosine-small(x) ∈ {y:ℝ| y = cosine(x)} 
BY
{ (RWO "int-rdiv-req" (-1) 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.  x1  :  (r(-1))/2  <  x
7.  |x|  <  (r1)/2
\mvdash{}  cosine-small(x)  \mmember{}  \{y:\mBbbR{}|  y  =  cosine(x)\} 


By

---

Latex:
(RWO  "int-rdiv-req"  (-1)  THEN  Auto)

---

Home Index