---

Step * 1 of Lemma sqs-rneq-or


1. x : ℝ
2. y : ℝ
3. x ≠ r0 ∨ y ≠ r0
4. v:ℤ × ℤ × {n':ℤ| 
              (1 ≤ n')
              ∧ (v = ((λn.eval a = x n in eval b = y n in   <a, b>) n') ∈ (ℤ × ℤ))
              ∧ (λp.let a,b = p in 4 <z |a| ∨b4 <z |b|) v = tt}  ∈ ℙ{[1 | i 0]}
⊢ ∃m:{1...}. ∀k:{m...}. (λp.let a,b = p in 4 <z |a| ∨b4 <z |b|) ((λn.eval a = x n in eval b = y n in   <a, b>) k) = tt
BY
{ (Reduce 0 THEN Thin (-1)) }

1
1. x : ℝ
2. y : ℝ
3. x ≠ r0 ∨ y ≠ r0
⊢ ∃m:{1...}. ∀k:{m...}. let a,b = eval a = x k in eval b = y k in   <a, b> in 4 <z |a| ∨b4 <z |b| = tt

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  x  \mneq{}  r0  \mvee{}  y  \mneq{}  r0
4.  v:\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  \{n':\mBbbZ{}| 
                            (1  \mleq{}  n')
                            \mwedge{}  (v  =  ((\mlambda{}n.eval  a  =  x  n  in  eval  b  =  y  n  in      <a,  b>)  n'))
                            \mwedge{}  (\mlambda{}p.let  a,b  =  p  in  4  <z  |a|  \mvee{}\msubb{}4  <z  |b|)  v  =  tt\}    \mmember{}  \mBbbP{}\{[1  |  i  0]\}
\mvdash{}  \mexists{}m:\{1...\}
      \mforall{}k:\{m...\}
          (\mlambda{}p.let  a,b  =  p  in  4  <z  |a|  \mvee{}\msubb{}4  <z  |b|)  ((\mlambda{}n.eval  a  =  x  n  in  eval  b  =  y  n  in      <a,  b>)  k)  =  tt


By

---

Latex:
(Reduce  0  THEN  Thin  (-1))

---

Home Index