---

Step * 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)
⊢ rcos(π/2(slower)) = r0
BY
{ (FLemma `unique-limit` [-1;-2] THEN Auto) }

1
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

---

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)
\mvdash{}  rcos(\mpi{}/2(slower))  =  r0


By

---

Latex:
(FLemma  `unique-limit`  [-1;-2]  THEN  Auto)

---

Home Index