---

Step * of Lemma rcos-positive-before-half-pi

∀x:{x:ℝ| x ∈ [r0, π/2)} . (r0 < rcos(x))
BY
{ (((Assert lim n→∞.rcos-seq(n) = π/2(slower) BY Auto) THEN (RWO  "halfpi-half-pi<" (-1) THENA Auto))
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN (Unhide THENA Auto)
   THEN Reduce -1
   THEN D -1
   THEN (Assert ⌜∃n:ℕ. (x ≤ rcos-seq(n))⌝⋅ THENM (ExRepD THEN InstLemma `rcos-seq-positive` [⌜n⌝]⋅ THEN Auto))) }

1
.....assertion..... 
1. lim n→∞.rcos-seq(n) = π/2
2. x : ℝ
3. r0 ≤ x
4. x < π/2
⊢ ∃n:ℕ. (x ≤ rcos-seq(n))

---

Latex:

---

Latex:
\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [r0,  \mpi{}/2)\}  .  (r0  <  rcos(x))


By

---

Latex:
(((Assert  lim  n\mrightarrow{}\minfty{}.rcos-seq(n)  =  \mpi{}/2(slower)  BY  Auto)  THEN  (RWO    "halfpi-half-pi<"  (-1)  THENA  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  (Unhide  THENA  Auto)
  THEN  Reduce  -1
  THEN  D  -1
  THEN  (Assert  \mkleeneopen{}\mexists{}n:\mBbbN{}.  (x  \mleq{}  rcos-seq(n))\mkleeneclose{}\mcdot{}
  THENM  (ExRepD  THEN  InstLemma  `rcos-seq-positive`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)
  ))

---

Home Index