---

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


1. b : ℕ+
2. x : ℕ+ ⟶ ℤ
3. ∀n,m:ℕ+.  (|(m * (x n)) - n * (x m)| ≤ ((2 * b) * (n + m)))
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|} 
⊢ (((|4| * |n| * |m|) * (2 * b) * (m + n)) + (|x m| * |m| * |-r1|) + (|x n| * |n| * |r2|)) ≤ ((|x n| * |x m|)
  * (2 * b * ((k * k) + 1))
  * (n + m))
BY
{ Assert ⌜(|4| * |n| * |m|) ≤ ((k * k) * |x n| * |x m|)⌝⋅ }

1
.....assertion..... 
1. b : ℕ+
2. x : ℕ+ ⟶ ℤ
3. ∀n,m:ℕ+.  (|(m * (x n)) - n * (x m)| ≤ ((2 * b) * (n + m)))
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|} 
⊢ (|4| * |n| * |m|) ≤ ((k * k) * |x n| * |x m|)

2
1. b : ℕ+
2. x : ℕ+ ⟶ ℤ
3. ∀n,m:ℕ+.  (|(m * (x n)) - n * (x m)| ≤ ((2 * b) * (n + m)))
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|} 
14. (|4| * |n| * |m|) ≤ ((k * k) * |x n| * |x m|)
⊢ (((|4| * |n| * |m|) * (2 * b) * (m + n)) + (|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.  \mforall{}n,m:\mBbbN{}\msupplus{}.    (|(m  *  (x  n))  -  n  *  (x  m)|  \mleq{}  ((2  *  b)  *  (n  +  m)))
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.  r2  :  \{r:\mBbbZ{}|  |r|  <  |x  m|\} 
\mvdash{}  (((|4|  *  |n|  *  |m|)  *  (2  *  b)  *  (m  +  n))  +  (|x  m|  *  |m|  *  |-r1|)  +  (|x  n|  *  |n|  *  |r2|))  \mleq{}  ((|x  n|
                                                                                                                                                                                            *  |x 
                                                                                                                                                                                                  m|)
    *  (2  *  b  *  ((k  *  k)  +  1))
    *  (n  +  m))


By

---

Latex:
Assert  \mkleeneopen{}(|4|  *  |n|  *  |m|)  \mleq{}  ((k  *  k)  *  |x  n|  *  |x  m|)\mkleeneclose{}\mcdot{}

---

Home Index