---

Step * 2 of Lemma sqs-rneq-or


1. x : ℝ
2. y : ℝ
3. ↓x ≠ r0 ∨ y ≠ r0
4. m : 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} 
5. m
= find-ge-val(λ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>;1)
∈ (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} )
⊢ x ≠ r0 ∨ y ≠ r0
BY
{ (Thin (-1) THEN D -1 THEN D -2 THEN Reduce -1) }

1
1. x : ℝ
2. y : ℝ
3. ↓x ≠ r0 ∨ y ≠ r0
4. v1 : ℤ
5. v2 : ℤ
6. m1 : {n':ℤ| 
         (1 ≤ n') ∧ (<v1, v2> = eval a = x n' in eval b = y n' in   <a, b> ∈ (ℤ × ℤ)) ∧ 4 <z |v1| ∨b4 <z |v2| = tt} 
⊢ x ≠ r0 ∨ y ≠ r0

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  \mdownarrow{}x  \mneq{}  r0  \mvee{}  y  \mneq{}  r0
4.  m  :  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\} 
5.  m
=  find-ge-val(\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>1)
\mvdash{}  x  \mneq{}  r0  \mvee{}  y  \mneq{}  r0


By

---

Latex:
(Thin  (-1)  THEN  D  -1  THEN  D  -2  THEN  Reduce  -1)

---

Home Index