---

Step * 2 1 of Lemma regular-upto-iff2


1. k : ℕ+
2. b : ℕ+
3. x : ℕ+ ⟶ ℤ
4. i : ℕ+b + 1
5. j : ℕ+b + 1
6. let j@0 = seq-max-lower(k;b;x) in
    let z = (r((x j@0) - 2 * k)/r((2 * k) * j@0)) in
    (((r((x i) - 2 * k)/r((2 * k) * i)) ≤ z) ∧ (z ≤ (r((x i) + (2 * k))/r((2 * k) * i))))
    ∧ ((r((x j) - 2 * k)/r((2 * k) * j)) ≤ z)
    ∧ (z ≤ (r((x j) + (2 * k))/r((2 * k) * j)))
⊢ |(i * (x j)) - j * (x i)| ≤ ((2 * k) * (i + j))
BY
{ ((MoveToConcl (-1) THEN RepUR ``let`` 0)
   THEN GenConcl ⌜(r((x seq-min-upper(k;b;x)) + (2 * k))/r((2 * k) * seq-min-upper(k;b;x))) = z ∈ ℝ⌝⋅
   THEN Auto) }

1
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))

---

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.  let  j@0  =  seq-max-lower(k;b;x)  in
        let  z  =  (r((x  j@0)  -  2  *  k)/r((2  *  k)  *  j@0))  in
        (((r((x  i)  -  2  *  k)/r((2  *  k)  *  i))  \mleq{}  z)  \mwedge{}  (z  \mleq{}  (r((x  i)  +  (2  *  k))/r((2  *  k)  *  i))))
        \mwedge{}  ((r((x  j)  -  2  *  k)/r((2  *  k)  *  j))  \mleq{}  z)
        \mwedge{}  (z  \mleq{}  (r((x  j)  +  (2  *  k))/r((2  *  k)  *  j)))
\mvdash{}  |(i  *  (x  j))  -  j  *  (x  i)|  \mleq{}  ((2  *  k)  *  (i  +  j))


By

---

Latex:
((MoveToConcl  (-1)  THEN  RepUR  ``let``  0)
  THEN  GenConcl  \mkleeneopen{}(r((x  seq-min-upper(k;b;x))  +  (2  *  k))/r((2  *  k)  *  seq-min-upper(k;b;x)))  =  z\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index