---

Step * 1 1 1 of Lemma reg-seq-inv_wf


1. b : ℕ+
2. x : ℕ+ ⟶ ℤ
3. b-regular-seq(x)
4. k : ℕ+
5. ∀m:ℕ+. ((2 * m) ≤ (k * |x m|))
6. ∀m:ℕ+. (¬((x m) = 0 ∈ ℤ))
7. reg-seq-inv(x) ∈ ℕ+ ⟶ ℤ
8. n : ℕ+
9. m : ℕ+
10. 0 < |x n|
11. 0 < |x m|
12. r1 : {r:ℤ| |r| < |x n|} 
13. (4 * n * n rem x n) = r1 ∈ {r:ℤ| |r| < |x n|} 
14. r2 : {r:ℤ| |r| < |x m|} 
15. (4 * m * m rem x m) = r2 ∈ {r:ℤ| |r| < |x m|} 
⊢ |((x m) * m * ((4 * n * n) - r1)) - (x n) * n * ((4 * m * m) - r2)| ≤ (|(x n) * (x m)|
  * (2 * b * ((k * k) + 1))
  * (n + m))
BY
{ ((Assert |((x m) * m * ((4 * n * n) - r1)) - (x n) * n * ((4 * m * m) - r2)| ≤ (|((x m) * m * 4 * n * n) - (x n)
                                                                                  * n
                                                                                  * 4
                                                                                  * m
                                                                                  * m|
           + |(x m) * m * (-r1)|
           + |(x n) * n * r2|) BY
          (RepeatFor 2 ((RWO "int-triangle-inequality<" 0 THENA Auto)) THEN RW IntNormC 0 THEN Auto))
   THEN (RWO "-1" 0 THENA Auto)
   THEN (RepeatFor 2 (Thin (-1)) THEN Thin (-2))⋅) }

1
1. b : ℕ+
2. x : ℕ+ ⟶ ℤ
3. b-regular-seq(x)
4. k : ℕ+
5. ∀m:ℕ+. ((2 * m) ≤ (k * |x m|))
6. ∀m:ℕ+. (¬((x m) = 0 ∈ ℤ))
7. reg-seq-inv(x) ∈ ℕ+ ⟶ ℤ
8. n : ℕ+
9. m : ℕ+
10. 0 < |x n|
11. 0 < |x m|
12. r1 : {r:ℤ| |r| < |x n|} 
13. r2 : {r:ℤ| |r| < |x m|} 
⊢ (|((x m) * m * 4 * n * n) - (x n) * n * 4 * m * m| + |(x m) * m * (-r1)| + |(x n) * n * r2|) ≤ (|(x n) * (x m)|
  * (2 * b * ((k * k) + 1))
  * (n + m))

---

Latex:

---

Latex:

1.  b  :  \mBbbN{}\msupplus{}
2.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  b-regular-seq(x)
4.  k  :  \mBbbN{}\msupplus{}
5.  \mforall{}m:\mBbbN{}\msupplus{}.  ((2  *  m)  \mleq{}  (k  *  |x  m|))
6.  \mforall{}m:\mBbbN{}\msupplus{}.  (\mneg{}((x  m)  =  0))
7.  reg-seq-inv(x)  \mmember{}  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
8.  n  :  \mBbbN{}\msupplus{}
9.  m  :  \mBbbN{}\msupplus{}
10.  0  <  |x  n|
11.  0  <  |x  m|
12.  r1  :  \{r:\mBbbZ{}|  |r|  <  |x  n|\} 
13.  (4  *  n  *  n  rem  x  n)  =  r1
14.  r2  :  \{r:\mBbbZ{}|  |r|  <  |x  m|\} 
15.  (4  *  m  *  m  rem  x  m)  =  r2
\mvdash{}  |((x  m)  *  m  *  ((4  *  n  *  n)  -  r1))  -  (x  n)  *  n  *  ((4  *  m  *  m)  -  r2)|  \mleq{}  (|(x  n)  *  (x  m)|
    *  (2  *  b  *  ((k  *  k)  +  1))
    *  (n  +  m))


By

---

Latex:
((Assert  |((x  m)  *  m  *  ((4  *  n  *  n)  -  r1))  -  (x  n)  *  n  *  ((4  *  m  *  m)  -  r2)|  \mleq{}  (|((x  m)
                                                                                                                                                                *  m
                                                                                                                                                                *  4
                                                                                                                                                                *  n
                                                                                                                                                                *  n)  -  (x  n)
                                                                                                                                                                *  n
                                                                                                                                                                *  4
                                                                                                                                                                *  m
                                                                                                                                                                *  m|
                  +  |(x  m)  *  m  *  (-r1)|
                  +  |(x  n)  *  n  *  r2|)  BY
                (RepeatFor  2  ((RWO  "int-triangle-inequality<"  0  THENA  Auto))  THEN  RW  IntNormC  0  THEN  Auto))
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (RepeatFor  2  (Thin  (-1))  THEN  Thin  (-2))\mcdot{})

---

Home Index