---

Step * 2 2 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
⊢ cosine-small(x) ∈ {y:ℝ| y = cosine(x)} 
BY
{ (Assert |x| < (r1)/2 BY
         (RWO "rabs-rless-iff" 0⋅
          THEN Auto
          THEN (Assert -((r1)/2) = (r(-1))/2 BY
                      (RWO "int-rdiv-req" 0 THEN Auto THEN nRNorm 0 THEN Auto))
          THEN Auto)) }

1
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)} 

---

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
\mvdash{}  cosine-small(x)  \mmember{}  \{y:\mBbbR{}|  y  =  cosine(x)\} 


By

---

Latex:
(Assert  |x|  <  (r1)/2  BY
              (RWO  "rabs-rless-iff"  0\mcdot{}
                THEN  Auto
                THEN  (Assert  -((r1)/2)  =  (r(-1))/2  BY
                                        (RWO  "int-rdiv-req"  0  THEN  Auto  THEN  nRNorm  0  THEN  Auto))
                THEN  Auto))

---

Home Index