---

Step * 2 1 1 of Lemma regular-upto-iff2


1. k : ℕ+
2. b : ℕ+
3. x : ℕ+ ⟶ ℤ
4. i : ℕ+b + 1
5. j : ℕ+b + 1
6. z : ℝ
7. (r((x seq-min-upper(k;b;x)) + (2 * k))/r((2 * k) * seq-min-upper(k;b;x))) = z ∈ ℝ
8. (r((x i) - 2 * k)/r((2 * k) * i)) ≤ (r((x seq-max-lower(k;b;x)) - 2 * k)/r((2 * k) * seq-max-lower(k;b;x)))
9. (r((x seq-max-lower(k;b;x)) - 2 * k)/r((2 * k) * seq-max-lower(k;b;x))) ≤ (r((x i) + (2 * k))/r((2 * k) * i))
10. (r((x j) - 2 * k)/r((2 * k) * j)) ≤ (r((x seq-max-lower(k;b;x)) - 2 * k)/r((2 * k) * seq-max-lower(k;b;x)))
11. (r((x seq-max-lower(k;b;x)) - 2 * k)/r((2 * k) * seq-max-lower(k;b;x))) ≤ (r((x j) + (2 * k))/r((2 * k) * j))
⊢ |(i * (x j)) - j * (x i)| ≤ ((2 * k) * (i + j))
BY
{ ((Assert ((r((x i) - 2 * k)/r((2 * k) * i)) ≤ (r((x j) + (2 * k))/r((2 * k) * j)))
          ∧ ((r((x j) - 2 * k)/r((2 * k) * j)) ≤ (r((x i) + (2 * k))/r((2 * k) * i))) BY
          Auto)
   THEN ThinVar `z'
   THEN (RWO "rleq-int-fractions" (-1) THENA Auto)) }

1
1. k : ℕ+
2. b : ℕ+
3. x : ℕ+ ⟶ ℤ
4. i : ℕ+b + 1
5. j : ℕ+b + 1
6. (r((x i) - 2 * k)/r((2 * k) * i)) ≤ (r((x seq-max-lower(k;b;x)) - 2 * k)/r((2 * k) * seq-max-lower(k;b;x)))
7. (r((x seq-max-lower(k;b;x)) - 2 * k)/r((2 * k) * seq-max-lower(k;b;x))) ≤ (r((x i) + (2 * k))/r((2 * k) * i))
8. (r((x j) - 2 * k)/r((2 * k) * j)) ≤ (r((x seq-max-lower(k;b;x)) - 2 * k)/r((2 * k) * seq-max-lower(k;b;x)))
9. (r((x seq-max-lower(k;b;x)) - 2 * k)/r((2 * k) * seq-max-lower(k;b;x))) ≤ (r((x j) + (2 * k))/r((2 * k) * j))
10. ((((x i) - 2 * k) * (2 * k) * j) ≤ (((x j) + (2 * k)) * (2 * k) * i))
∧ ((((x j) - 2 * k) * (2 * k) * i) ≤ (((x i) + (2 * k)) * (2 * k) * j))
⊢ |(i * (x j)) - j * (x i)| ≤ ((2 * k) * (i + j))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  b  :  \mBbbN{}\msupplus{}
3.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
4.  i  :  \mBbbN{}\msupplus{}b  +  1
5.  j  :  \mBbbN{}\msupplus{}b  +  1
6.  z  :  \mBbbR{}
7.  (r((x  seq-min-upper(k;b;x))  +  (2  *  k))/r((2  *  k)  *  seq-min-upper(k;b;x)))  =  z
8.  (r((x  i)  -  2  *  k)/r((2  *  k)  *  i))  \mleq{}  (r((x  seq-max-lower(k;b;x))  -  2  *  k)/r((2  *  k)
*  seq-max-lower(k;b;x)))
9.  (r((x  seq-max-lower(k;b;x))  -  2  *  k)/r((2  *  k)  *  seq-max-lower(k;b;x)))  \mleq{}  (r((x  i)
+  (2  *  k))/r((2  *  k)  *  i))
10.  (r((x  j)  -  2  *  k)/r((2  *  k)  *  j))  \mleq{}  (r((x  seq-max-lower(k;b;x))  -  2  *  k)/r((2  *  k)
*  seq-max-lower(k;b;x)))
11.  (r((x  seq-max-lower(k;b;x))  -  2  *  k)/r((2  *  k)  *  seq-max-lower(k;b;x)))  \mleq{}  (r((x  j)
+  (2  *  k))/r((2  *  k)  *  j))
\mvdash{}  |(i  *  (x  j))  -  j  *  (x  i)|  \mleq{}  ((2  *  k)  *  (i  +  j))


By

---

Latex:
((Assert  ((r((x  i)  -  2  *  k)/r((2  *  k)  *  i))  \mleq{}  (r((x  j)  +  (2  *  k))/r((2  *  k)  *  j)))
                \mwedge{}  ((r((x  j)  -  2  *  k)/r((2  *  k)  *  j))  \mleq{}  (r((x  i)  +  (2  *  k))/r((2  *  k)  *  i)))  BY
                Auto)
  THEN  ThinVar  `z'
  THEN  (RWO  "rleq-int-fractions"  (-1)  THENA  Auto))

---

Home Index