---

Step * of Lemma radd_rcos-Taylor

∀b:ℝ. (|radd_rcos(b) - π/2(slower)| ≤ (|b - π/2(slower)|^3/r(2)))
BY
{ ((D 0 THENA Auto)
   THEN BLemma  `rleq-iff-all-rless`
   THEN Auto
   THEN (InstLemma `Taylor-theorem`
          [⌜(-∞, ∞)⌝;⌜2⌝;⌜λ2i x.if (i =z 0) then radd_rcos(x)
                          if (i =z 1) then r1 - rsin(x)
                          if (i =z 2) then -(rcos(x))
                          else rsin(x)
                          fi ⌝;⌜π/2(slower)⌝;⌜b⌝;⌜e⌝]⋅
         THENA (Reduce 0 THEN Auto THEN Try ((IntSegCases 3 THEN Reduce 0 THEN Auto THEN RWO  "-2" 0 THEN Auto)))
         )
   THEN ExRepD) }

1
1. b : ℝ
2. e : {e:ℝ| r0 < e} 
3. c : ℝ
4. rmin(π/2(slower);b) ≤ c
5. c ≤ rmax(π/2(slower);b)
6. |Taylor-remainder((-∞, ∞);2;b;π/2(slower);k,x.if (k =z 0) then radd_rcos(x)
if (k =z 1) then r1 - rsin(x)
if (k =z 2) then -(rcos(x))
else rsin(x)
fi ) - (b - c^2
* (if (2 + 1 =z 0) then radd_rcos(c)
  if (2 + 1 =z 1) then r1 - rsin(c)
  if (2 + 1 =z 2) then -(rcos(c))
  else rsin(c)
  fi /r((2)!)))
* (b - π/2(slower))| ≤ e
⊢ |radd_rcos(b) - π/2(slower)| ≤ ((|b - π/2(slower)|^3/r(2)) + e)

---

Latex:

---

Latex:
\mforall{}b:\mBbbR{}.  (|radd\_rcos(b)  -  \mpi{}/2(slower)|  \mleq{}  (|b  -  \mpi{}/2(slower)|\^{}3/r(2)))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  BLemma    `rleq-iff-all-rless`
  THEN  Auto
  THEN  (InstLemma  `Taylor-theorem`
                [\mkleeneopen{}(-\minfty{},  \minfty{})\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i  x.if  (i  =\msubz{}  0)  then  radd\_rcos(x)
                                                if  (i  =\msubz{}  1)  then  r1  -  rsin(x)
                                                if  (i  =\msubz{}  2)  then  -(rcos(x))
                                                else  rsin(x)
                                                fi  \mkleeneclose{};\mkleeneopen{}\mpi{}/2(slower)\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
              THENA  (Reduce  0
                            THEN  Auto
                            THEN  Try  ((IntSegCases  3  THEN  Reduce  0  THEN  Auto  THEN  RWO    "-2"  0  THEN  Auto)))
              )
  THEN  ExRepD)

---

Home Index