---

Step * 1 2 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
⊢ False
BY
{ (InstHyp [⌜λn.(r1/r(n + 1))⌝;⌜P⌝] (-2)⋅ THEN Auto THEN ExRepD THEN All Reduce) }

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' = ff
⊢ lim n→∞.(r1/r(n + 1)) = r0

2
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. z : {z:ℝ| P z = P x'} 
7. n : ℕ
8. z = (r1/r(n + 1))
⊢ False

---

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
\mvdash{}  False


By

---

Latex:
(InstHyp  [\mkleeneopen{}\mlambda{}n.(r1/r(n  +  1))\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto  THEN  ExRepD  THEN  All  Reduce)

---

Home Index