---

Step * 1 2 1 1 1 of Lemma radd_rcos-Taylor


1. b : ℝ
2. e : {e:ℝ| r0 < e} 
3. c : ℝ
4. rmin(π/2(slower);b) ≤ c
5. c ≤ rmax(π/2(slower);b)
6. z : ℝ
⊢ (r(2) * |(b + -(c)^2 * rsin(c)/r(2))|) ≤ |-(π/2(slower)) + b|^2
BY
{ ((Assert |r(2)| = r(2) BY
          (BLemma `rabs-of-nonneg`  THEN Auto))
   THEN (Assert r0 < |r(2)| BY
               (RWO "-1" 0 THEN Auto))
   THEN ((RWO "rabs-rdiv" 0 THENA Auto) THEN (RWO "rabs-rmul" 0 THENA Auto))
   THEN (RWO "-2" 0 THEN Auto)
   THEN nRNorm 0) }

1
1. b : ℝ
2. e : {e:ℝ| r0 < e} 
3. c : ℝ
4. rmin(π/2(slower);b) ≤ c
5. c ≤ rmax(π/2(slower);b)
6. z : ℝ
7. |r(2)| = r(2)
8. r0 < |r(2)|
⊢ (|b + -(c)^2| * |rsin(c)|) ≤ |-(π/2(slower)) + b|^2

---

Latex:

---

Latex:

1.  b  :  \mBbbR{}
2.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
3.  c  :  \mBbbR{}
4.  rmin(\mpi{}/2(slower);b)  \mleq{}  c
5.  c  \mleq{}  rmax(\mpi{}/2(slower);b)
6.  z  :  \mBbbR{}
\mvdash{}  (r(2)  *  |(b  +  -(c)\^{}2  *  rsin(c)/r(2))|)  \mleq{}  |-(\mpi{}/2(slower))  +  b|\^{}2


By

---

Latex:
((Assert  |r(2)|  =  r(2)  BY
                (BLemma  `rabs-of-nonneg`    THEN  Auto))
  THEN  (Assert  r0  <  |r(2)|  BY
                          (RWO  "-1"  0  THEN  Auto))
  THEN  ((RWO  "rabs-rdiv"  0  THENA  Auto)  THEN  (RWO  "rabs-rmul"  0  THENA  Auto))
  THEN  (RWO  "-2"  0  THEN  Auto)
  THEN  nRNorm  0)

---

Home Index