---

Step * 1 1 1 2 1 1 of Lemma pseudo-positive-is-positive-proof2


1. ∀a:ℕ*. ((∀c:ℕ*. ((¬¬(∃n:ℕ. (¬((a n) = (c n) ∈ ℤ)))) ∨ (¬¬(∃n:ℕ. (¬(0 = (c n) ∈ ℤ)))))) ⇒ (∃n:ℕ. 0 < a n))
2. x : ℝ
3. pseudo-positive(x)
4. d : ∀n:ℕ. ((|x| < (r1)/2^n) ∨ ((r1)/2^(n + 1) < |x|))
5. ∃n:ℕ. 0 < if isl(d n) then 0 else 1 fi 
6. ∃n:ℕ. (↑isr(d n))
⊢ r0 < x
BY
{ (D -1 THEN MoveToConcl  (-1) THEN (GenConclTerm ⌜d n⌝⋅ THENA Auto) THEN (D -2 THEN Reduce 0) THEN Auto) }

1
1. ∀a:ℕ*. ((∀c:ℕ*. ((¬¬(∃n:ℕ. (¬((a n) = (c n) ∈ ℤ)))) ∨ (¬¬(∃n:ℕ. (¬(0 = (c n) ∈ ℤ)))))) ⇒ (∃n:ℕ. 0 < a n))
2. x : ℝ
3. pseudo-positive(x)
4. d : ∀n:ℕ. ((|x| < (r1)/2^n) ∨ ((r1)/2^(n + 1) < |x|))
5. ∃n:ℕ. 0 < if isl(d n) then 0 else 1 fi 
6. n : ℕ
7. y : (r1)/2^(n + 1) < |x|
8. (d n) = (inr y ) ∈ ((|x| < (r1)/2^n) ∨ ((r1)/2^(n + 1) < |x|))
9. True
⊢ r0 < x

---

Latex:

---

Latex:

1.  \mforall{}a:\mBbbN{}*
          ((\mforall{}c:\mBbbN{}*.  ((\mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  (\mneg{}((a  n)  =  (c  n)))))  \mvee{}  (\mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  (\mneg{}(0  =  (c  n)))))))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  0  <  a  n))
2.  x  :  \mBbbR{}
3.  pseudo-positive(x)
4.  d  :  \mforall{}n:\mBbbN{}.  ((|x|  <  (r1)/2\^{}n)  \mvee{}  ((r1)/2\^{}(n  +  1)  <  |x|))
5.  \mexists{}n:\mBbbN{}.  0  <  if  isl(d  n)  then  0  else  1  fi 
6.  \mexists{}n:\mBbbN{}.  (\muparrow{}isr(d  n))
\mvdash{}  r0  <  x


By

---

Latex:
(D  -1
  THEN  MoveToConcl    (-1)
  THEN  (GenConclTerm  \mkleeneopen{}d  n\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  -2  THEN  Reduce  0)
  THEN  Auto)

---

Home Index