---

Step * of Lemma rcos-half-pi

rcos(π/2(slower)) = r0
BY
{ ((Assert lim n→∞.rcos-seq(n) = π/2(slower) BY
          Auto)
   THEN (InstLemma `total-function-limit` [⌜λ2x.rcos(x)⌝]⋅ THENA Auto)
   THEN (FHyp (-1) [1] THENA (Auto THEN RWO "-1" 0 THEN Auto))
   THEN Thin(-2)) }

1
1. lim n→∞.rcos-seq(n) = π/2(slower)
2. lim n→∞.rcos(rcos-seq(n)) = rcos(π/2(slower))
⊢ rcos(π/2(slower)) = r0

---

Latex:

---

Latex:
rcos(\mpi{}/2(slower))  =  r0


By

---

Latex:
((Assert  lim  n\mrightarrow{}\minfty{}.rcos-seq(n)  =  \mpi{}/2(slower)  BY
                Auto)
  THEN  (InstLemma  `total-function-limit`  [\mkleeneopen{}\mlambda{}\msubtwo{}x.rcos(x)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (FHyp  (-1)  [1]  THENA  (Auto  THEN  RWO  "-1"  0  THEN  Auto))
  THEN  Thin(-2))

---

Home Index