---

Step * 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 : ℕ+
⊢ |(m * (reg-seq-inv(x) n)) - n * (reg-seq-inv(x) m)| ≤ ((2 * b * ((k * k) + 1)) * (n + m))
BY
{ ((Assert 0 < |x n| BY
          (InstHyp [⌜n⌝] 6⋅ THEN Auto THEN (RWO "absval_unfold" 0 THENA Auto) THEN AutoSplit))
   THEN (Assert 0 < |x m| BY
               (InstHyp [⌜m⌝] 6⋅ THEN Auto THEN (RWO "absval_unfold" 0 THENA Auto) THEN AutoSplit))
   THEN ((Using [`n', ⌜|(x n) * (x m)|⌝] (BLemma `mul_cancel_in_le`)⋅ THENA (Auto THEN RWO "absval_mul" 0 THEN Auto))
         THEN ((RWO "absval_mul<" 0 THENA Auto) THEN (RWO "left_mul_subtract_distrib" 0 THENA Auto))⋅
         )⋅⋅) }

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|
⊢ |(((x n) * (x m)) * m * (reg-seq-inv(x) n)) - ((x n) * (x m)) * n * (reg-seq-inv(x) m)| ≤ (|(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{}
\mvdash{}  |(m  *  (reg-seq-inv(x)  n))  -  n  *  (reg-seq-inv(x)  m)|  \mleq{}  ((2  *  b  *  ((k  *  k)  +  1))  *  (n  +  m))


By

---

Latex:
((Assert  0  <  |x  n|  BY
                (InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  6\mcdot{}  THEN  Auto  THEN  (RWO  "absval\_unfold"  0  THENA  Auto)  THEN  AutoSplit))
  THEN  (Assert  0  <  |x  m|  BY
                          (InstHyp  [\mkleeneopen{}m\mkleeneclose{}]  6\mcdot{}  THEN  Auto  THEN  (RWO  "absval\_unfold"  0  THENA  Auto)  THEN  AutoSplit))
  THEN  ((Using  [`n',  \mkleeneopen{}|(x  n)  *  (x  m)|\mkleeneclose{}]  (BLemma  `mul\_cancel\_in\_le`)\mcdot{}
                THENA  (Auto  THEN  RWO  "absval\_mul"  0  THEN  Auto)
                )
              THEN  ((RWO  "absval\_mul<"  0  THENA  Auto)  THEN  (RWO  "left\_mul\_subtract\_distrib"  0  THENA  Auto))\mcdot{}
              )\mcdot{}\mcdot{})

---

Home Index