---

Step * 1 1 1 1 2 2 1 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. c : ℕ*
6. if (∀i∈upto(n).(nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) i =z c i))_b then x else r0 fi ↓ as n→∞
⇒ cauchy(n.if (∀i∈upto(n).(nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) i =z c i))_b then x else r0 fi )
7. y : ℝ
8. lim n→∞.if (∀i∈upto(n).(nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) i =z c i))_b then x else r0 fi  = y
9. ∀y:ℝ. ((¬(x = y)) ∨ (¬(y = r0)))
10. ¬(∃n:ℕ. (¬((nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) n) = (c n) ∈ ℤ)))
11. ∀n:ℕ. ((nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) n) = (c n) ∈ ℤ)
⊢ x = y
BY
{ (InstLemma  `converges-to_functionality` [
   ⌜λ2n.if (∀i∈upto(n).(nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) i =z c i))_b then x else r0 fi ⌝;⌜λ2n.x⌝;⌜y⌝;
   ⌜y⌝]⋅
   THENA 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. c : ℕ*
6. if (∀i∈upto(n).(nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) i =z c i))_b then x else r0 fi ↓ as n→∞
⇒ cauchy(n.if (∀i∈upto(n).(nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) i =z c i))_b then x else r0 fi )
7. y : ℝ
8. lim n→∞.if (∀i∈upto(n).(nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) i =z c i))_b then x else r0 fi  = y
9. ∀y:ℝ. ((¬(x = y)) ∨ (¬(y = r0)))
10. ¬(∃n:ℕ. (¬((nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) n) = (c n) ∈ ℤ)))
11. ∀n:ℕ. ((nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) n) = (c n) ∈ ℤ)
12. n : ℕ
13. ¬↑(∀i∈upto(n).(nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) i =z c i))_b
⊢ if (∀i∈upto(n).(nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) i =z c i))_b then x else r0 fi  = x

2
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. c : ℕ*
6. if (∀i∈upto(n).(nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) i =z c i))_b then x else r0 fi ↓ as n→∞
⇒ cauchy(n.if (∀i∈upto(n).(nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) i =z c i))_b then x else r0 fi )
7. y : ℝ
8. lim n→∞.if (∀i∈upto(n).(nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) i =z c i))_b then x else r0 fi  = y
9. ∀y:ℝ. ((¬(x = y)) ∨ (¬(y = r0)))
10. ¬(∃n:ℕ. (¬((nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) n) = (c n) ∈ ℤ)))
11. ∀n:ℕ. ((nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) n) = (c n) ∈ ℤ)
12. lim n→∞.if (∀i∈upto(n).(nat-star-retract(λn.if isl(d n) then 0 else 1 fi ) i =z c i))_b then x else r0 fi  = y
⇒ lim n→∞.x = y
⊢ x = y

---

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.  c  :  \mBbbN{}*
6.  if  (\mforall{}i\mmember{}upto(n).(nat-star-retract(\mlambda{}n.if  isl(d  n)  then  0  else  1  fi  )  i  =\msubz{}  c  i))\_b
then  x
else  r0
fi  \mdownarrow{}  as  n\mrightarrow{}\minfty{}
{}\mRightarrow{}  cauchy(n.if  (\mforall{}i\mmember{}upto(n).(nat-star-retract(\mlambda{}n.if  isl(d  n)  then  0  else  1  fi  )  i  =\msubz{}  c  i))\_b
      then  x
      else  r0
      fi  )
7.  y  :  \mBbbR{}
8.  lim  n\mrightarrow{}\minfty{}.if  (\mforall{}i\mmember{}upto(n).(nat-star-retract(\mlambda{}n.if  isl(d  n)  then  0  else  1  fi  )  i  =\msubz{}  c  i))\_b
then  x
else  r0
fi    =  y
9.  \mforall{}y:\mBbbR{}.  ((\mneg{}(x  =  y))  \mvee{}  (\mneg{}(y  =  r0)))
10.  \mneg{}(\mexists{}n:\mBbbN{}.  (\mneg{}((nat-star-retract(\mlambda{}n.if  isl(d  n)  then  0  else  1  fi  )  n)  =  (c  n))))
11.  \mforall{}n:\mBbbN{}.  ((nat-star-retract(\mlambda{}n.if  isl(d  n)  then  0  else  1  fi  )  n)  =  (c  n))
\mvdash{}  x  =  y


By

---

Latex:
(InstLemma    `converges-to\_functionality`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.if  (\mforall{}i\mmember{}upto(n).(nat-star-retract(\mlambda{}n.if  isl(d  n)
                                                                                                                                                                      then  0
                                                                                                                                                                      else  1
                                                                                                                                                                      fi  ) 
                                                                                                                              i  =\msubz{}  c  i))\_b
                                                                                      then  x
                                                                                      else  r0
                                                                                      fi  \mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n.x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}
  THENA  Auto
  )

---

Home Index