---

Step * 1 1 1 1 of Lemma rcos-half-pi


1. lim n→∞.rcos-seq(n) = π/2(slower)
2. lim n→∞.rcos(rcos-seq(n)) = rcos(π/2(slower))
3. lim n→∞.rcos-seq(n + 1) = π/2(slower) + rcos(π/2(slower))
4. lim n→∞.rcos-seq(n + 1) = π/2(slower)
5. π/2(slower) = (π/2(slower) + rcos(π/2(slower)))
⊢ rcos(π/2(slower)) = r0
BY
{ (nRAdd ⌜-(π/2(slower))⌝ (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  lim  n\mrightarrow{}\minfty{}.rcos-seq(n)  =  \mpi{}/2(slower)
2.  lim  n\mrightarrow{}\minfty{}.rcos(rcos-seq(n))  =  rcos(\mpi{}/2(slower))
3.  lim  n\mrightarrow{}\minfty{}.rcos-seq(n  +  1)  =  \mpi{}/2(slower)  +  rcos(\mpi{}/2(slower))
4.  lim  n\mrightarrow{}\minfty{}.rcos-seq(n  +  1)  =  \mpi{}/2(slower)
5.  \mpi{}/2(slower)  =  (\mpi{}/2(slower)  +  rcos(\mpi{}/2(slower)))
\mvdash{}  rcos(\mpi{}/2(slower))  =  r0


By

---

Latex:
(nRAdd  \mkleeneopen{}-(\mpi{}/2(slower))\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)

---

Home Index