---

Step * 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))
⊢ rcos(π/2(slower)) = r0
BY
{ ((InstLemma `limit-shift` [⌜1⌝]⋅ THENA Auto) THEN (FHyp (-1) [1] THENA Auto) THEN Thin (-2)) }

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


By

---

Latex:
((InstLemma  `limit-shift`  [\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  (FHyp  (-1)  [1]  THENA  Auto)  THEN  Thin  (-2))

---

Home Index