---

Step * of Lemma sqs-rneq-or

∀x,y:ℝ.  SqStable(x ≠ r0 ∨ y ≠ r0)
BY
{ (Intros
   THEN (D 0 THENA Auto)
   THEN (Evaluate ⌜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} )⌝⋅
         THENA (SqExRepD THEN Auto)
         )) }

1
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

2
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

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    SqStable(x  \mneq{}  r0  \mvee{}  y  \mneq{}  r0)


By

---

Latex:
(Intros
  THEN  (D  0  THENA  Auto)
  THEN  (Evaluate  \mkleeneopen{}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)\mkleeneclose{}\mcdot{}
              THENA  (SqExRepD  THEN  Auto)
              ))

---

Home Index