---

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

.....set predicate..... 
1. ∀a:ℕ*. ((∀c:ℕ*. ((¬¬(∃n:ℕ. (¬((a n) = (c n) ∈ ℤ)))) ∨ (¬¬(∃n:ℕ. (¬(0 = (c n) ∈ ℤ)))))) ⇒ (∃n:ℕ. 0 < a n))
2. x : ℝ
3. pseudo-positive(x)
⊢ r0 < x
BY
{ (Assert ∀n:ℕ. ((|x| < (r1)/2^n) ∨ ((r1)/2^(n + 1) < |x|)) BY
         (((D 0 THENA Auto) THEN InstLemma  `rless-cases`[⌜(r1)/2^(n + 1)⌝;⌜(r1)/2^n⌝;⌜|x|⌝]⋅)
          THEN Auto
          THEN Try ((DOr (-1)⋅ THEN Auto))
          THEN (Assert 2^n < 2^(n + 1) BY
                      (BLemma  `exp-increasing`  THEN Auto))
          THEN RWO "int-rdiv-req" 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. ∀n:ℕ. ((|x| < (r1)/2^n) ∨ ((r1)/2^(n + 1) < |x|))
⊢ r0 < x

---

Latex:

---

Latex:
.....set  predicate..... 
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)
\mvdash{}  r0  <  x


By

---

Latex:
(Assert  \mforall{}n:\mBbbN{}.  ((|x|  <  (r1)/2\^{}n)  \mvee{}  ((r1)/2\^{}(n  +  1)  <  |x|))  BY
              (((D  0  THENA  Auto)  THEN  InstLemma    `rless-cases`[\mkleeneopen{}(r1)/2\^{}(n  +  1)\mkleeneclose{};\mkleeneopen{}(r1)/2\^{}n\mkleeneclose{};\mkleeneopen{}|x|\mkleeneclose{}]\mcdot{})
                THEN  Auto
                THEN  Try  ((DOr  (-1)\mcdot{}  THEN  Auto))
                THEN  (Assert  2\^{}n  <  2\^{}(n  +  1)  BY
                                        (BLemma    `exp-increasing`    THEN  Auto))
                THEN  RWO  "int-rdiv-req"  0
                THEN  Auto))

---

Home Index