---

Step * 1 of Lemma rcos-half-pi


1. lim n→∞.rcos-seq(n) = π/2(slower)
2. lim n→∞.rcos(rcos-seq(n)) = rcos(π/2(slower))
⊢ rcos(π/2(slower)) = r0
BY
{ ((FLemma `radd-limit` [1;2] THENA Auto) THEN (RWO "rcos-seq-step<" (-1) THENA 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))
⊢ 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))
\mvdash{}  rcos(\mpi{}/2(slower))  =  r0


By

---

Latex:
((FLemma  `radd-limit`  [1;2]  THENA  Auto)  THEN  (RWO  "rcos-seq-step<"  (-1)  THENA  Auto))

---

Home Index