---

Step * 1 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' = tt
⊢ lim n→∞.(r(-1)/r(n + 1)) = r0
BY
{ ((D 0 THENA Auto) THEN D 0 With ⌜k⌝  THEN Auto) }

1
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' = tt
6. k : ℕ+
7. n : ℕ
8. k ≤ n
⊢ |(r(-1)/r(n + 1)) - r0| ≤ (r1/r(k))

---

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'  =  tt
\mvdash{}  lim  n\mrightarrow{}\minfty{}.(r(-1)/r(n  +  1))  =  r0


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  0  With  \mkleeneopen{}k\mkleeneclose{}    THEN  Auto)

---

Home Index