---

Step * 1 2 1 1 of Lemma not-all-nonneg-or-nonpos


1. P : ℝ ⟶ 𝔹
2. ∀x:ℝ. ((P x = tt ⇒ (r0 ≤ x)) ∧ (P x = ff ⇒ (x ≤ r0)))
3. x' : {x':ℝ| x' = r0} 
4. ∀g:ℕ ⟶ ℝ. (lim n→∞.g n = r0 ⇒ (∀P:ℝ ⟶ 𝔹. ∃z:{z:ℝ| P z = P x'} . (∃n:ℕ [(z = (g n))])))
5. P x' = ff
6. k : ℕ+
7. n : ℕ
8. k ≤ n
⊢ |(r1/r(n + 1)) - r0| ≤ (r1/r(k))
BY
{ ((Assert |(r1/r(n + 1)) - r0| = (r1/r(n + 1)) BY
          ((GenConcl ⌜r(n + 1) = z ∈ {z:ℝ| r0 < z} ⌝⋅ THENA Auto)
           THEN RWO "rabs-of-nonneg" 0
           THEN Auto
           THEN nRMul ⌜z⌝ 0⋅
           THEN Auto))
   THEN RWO  "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  P  :  \mBbbR{}  {}\mrightarrow{}  \mBbbB{}
2.  \mforall{}x:\mBbbR{}.  ((P  x  =  tt  {}\mRightarrow{}  (r0  \mleq{}  x))  \mwedge{}  (P  x  =  ff  {}\mRightarrow{}  (x  \mleq{}  r0)))
3.  x'  :  \{x':\mBbbR{}|  x'  =  r0\} 
4.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  (lim  n\mrightarrow{}\minfty{}.g  n  =  r0  {}\mRightarrow{}  (\mforall{}P:\mBbbR{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}z:\{z:\mBbbR{}|  P  z  =  P  x'\}  .  (\mexists{}n:\mBbbN{}  [(z  =  (g  n))])))
5.  P  x'  =  ff
6.  k  :  \mBbbN{}\msupplus{}
7.  n  :  \mBbbN{}
8.  k  \mleq{}  n
\mvdash{}  |(r1/r(n  +  1))  -  r0|  \mleq{}  (r1/r(k))


By

---

Latex:
((Assert  |(r1/r(n  +  1))  -  r0|  =  (r1/r(n  +  1))  BY
                ((GenConcl  \mkleeneopen{}r(n  +  1)  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
                  THEN  RWO  "rabs-of-nonneg"  0
                  THEN  Auto
                  THEN  nRMul  \mkleeneopen{}z\mkleeneclose{}  0\mcdot{}
                  THEN  Auto))
  THEN  RWO    "-1"  0
  THEN  Auto)

---

Home Index