---

Step * 1 2 1 1 of Lemma radd_rcos-Taylor

.....assertion..... 
1. b : ℝ
2. e : {e:ℝ| r0 < e} 
3. c : ℝ
4. rmin(π/2(slower);b) ≤ c
5. c ≤ rmax(π/2(slower);b)
6. z : ℝ
⊢ |b - c^2 * (rsin(c)/r((2)!))| ≤ (|b - π/2(slower)|^2/r(2))
BY
{ ((Subst' (2)! ~ 2 0 THENA Auto) THEN (nRMul ⌜r(2)⌝ 0⋅ THENA Auto)) }

1
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

---

Latex:

---

Latex:
.....assertion..... 
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{}  |b  -  c\^{}2  *  (rsin(c)/r((2)!))|  \mleq{}  (|b  -  \mpi{}/2(slower)|\^{}2/r(2))


By

---

Latex:
((Subst'  (2)!  \msim{}  2  0  THENA  Auto)  THEN  (nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}  THENA  Auto))

---

Home Index