---

Step * 1 2 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
6. z : {z:ℝ| P z = P x'} 
7. n : ℕ
8. z = (r1/r(n + 1))
⊢ False
BY
{ ((InstHyp [⌜z⌝] 2⋅ THENA Auto) THEN D -1 THEN (D -1 THENA 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' = ff
6. z : {z:ℝ| P z = P x'} 
7. n : ℕ
8. z = (r1/r(n + 1))
9. P z = tt ⇒ (r0 ≤ z)
10. z ≤ r0
⊢ 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
6.  z  :  \{z:\mBbbR{}|  P  z  =  P  x'\} 
7.  n  :  \mBbbN{}
8.  z  =  (r1/r(n  +  1))
\mvdash{}  False


By

---

Latex:
((InstHyp  [\mkleeneopen{}z\mkleeneclose{}]  2\mcdot{}  THENA  Auto)  THEN  D  -1  THEN  (D  -1  THENA  Auto))

---

Home Index