---

Step * 1 1 of Lemma sqs-rneq-or


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
BY
{ (RepeatFor 2 (D -1)
   THEN (RWO "rless-iff4" (-1) THENA Auto)
   THEN RepUR ``int-to-real`` -1
   THEN RepeatFor 2 (ParallelLast)
   THEN (RW IntNormC (-1) THENA Auto)
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN Reduce 0
   THEN (RWO "eqtt_to_assert" 0 THENA Auto)
   THEN (RW assert_pushdownC 0 THENA Auto)) }

1
1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. ∀m:{n...}. (x m) + 4 < 2 * m * 0
5. k : {n...}
6. 4 + (x k) < 0
⊢ 4 < |x k| ∨ 4 < |y k|

2
1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. ∀m:{n...}. (2 * m * 0) + 4 < x m
5. k : {n...}
6. 4 < x k
⊢ 4 < |x k| ∨ 4 < |y k|

3
1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. ∀m:{n...}. (y m) + 4 < 2 * m * 0
5. k : {n...}
6. 4 + (y k) < 0
⊢ 4 < |x k| ∨ 4 < |y k|

4
1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. ∀m:{n...}. (2 * m * 0) + 4 < y m
5. k : {n...}
6. 4 < y k
⊢ 4 < |x k| ∨ 4 < |y k|

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  x  \mneq{}  r0  \mvee{}  y  \mneq{}  r0
\mvdash{}  \mexists{}m:\{1...\}.  \mforall{}k:\{m...\}.  let  a,b  =  eval  a  =  x  k  in  eval  b  =  y  k  in      <a,  b>  in  4  <z  |a|  \mvee{}\msubb{}4  <z  |b|  =  \000Ctt


By

---

Latex:
(RepeatFor  2  (D  -1)
  THEN  (RWO  "rless-iff4"  (-1)  THENA  Auto)
  THEN  RepUR  ``int-to-real``  -1
  THEN  RepeatFor  2  (ParallelLast)
  THEN  (RW  IntNormC  (-1)  THENA  Auto)
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  Reduce  0
  THEN  (RWO  "eqtt\_to\_assert"  0  THENA  Auto)
  THEN  (RW  assert\_pushdownC  0  THENA  Auto))

---

Home Index