---

Step * 2 1 1 1 of Lemma reg-seq-nexp_wf


1. x : ℝ
2. k : ℕ+
3. 1 ≤ 2^k - 1
4. v : {3...}
5. canon-bnd(x) = v ∈ {k:{3...}| ∀n:ℕ+. (|x n| ≤ (n * k))} 
6. 1 ≤ 2^(k - 1)
7. n : ℕ+
8. m : ℕ+
9. ∀n:ℕ+. (|x n| ≤ (n * v))
10. 0 ≤ (v^(k - 1) ÷ 2^(k - 1))
11. 0 ≤ (k * ((v^(k - 1) ÷ 2^(k - 1)) + 1))
⊢ |(m * ((x n)^k ÷ (2 * n)^(k - 1))) - n * ((x m)^k ÷ (2 * m)^(k - 1))| ≤ ((2
  * ((k * ((v^(k - 1) ÷ 2^(k - 1)) + 1)) + 1))
  * (n + m))
BY
{ (((GenConcl ⌜(k * ((v^(k - 1) ÷ 2^(k - 1)) + 1)) = B ∈ ℕ⌝⋅ THENA Auto) THEN (GenConcl ⌜(n + m) = c ∈ ℕ+⌝⋅ THENA Auto))
   THEN (Assert 0 < (2 * n)^(k - 1) ∧ 0 < (2 * m)^(k - 1) BY
               Auto)
   THEN (GenConcl ⌜(2 * m)^(k - 1) = M ∈ ℕ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(2 * n)^(k - 1) = N ∈ ℕ⌝⋅ THENA Auto)
   THEN (MulAbs ⌜N⌝ 0 ⋅ THENA Auto)
   THEN (MulAbs ⌜M⌝ 0 ⋅ THENA Auto)
   THEN (RW DivRemC 0 THENA Auto)
   THEN RepeatFor 2 ((GenRem THENA Auto))
   THEN (RW IntNormC 0 THENA Auto)) }

1
1. x : ℝ
2. k : ℕ+
3. 1 ≤ 2^k - 1
4. v : {3...}
5. canon-bnd(x) = v ∈ {k:{3...}| ∀n:ℕ+. (|x n| ≤ (n * k))} 
6. 1 ≤ 2^(k - 1)
7. n : ℕ+
8. m : ℕ+
9. ∀n:ℕ+. (|x n| ≤ (n * v))
10. 0 ≤ (v^(k - 1) ÷ 2^(k - 1))
11. 0 ≤ (k * ((v^(k - 1) ÷ 2^(k - 1)) + 1))
12. B : ℕ
13. (k * ((v^(k - 1) ÷ 2^(k - 1)) + 1)) = B ∈ ℕ
14. c : ℕ+
15. (n + m) = c ∈ ℕ+
16. 0 < (2 * n)^(k - 1) ∧ 0 < (2 * m)^(k - 1)
17. M : ℕ
18. (2 * m)^(k - 1) = M ∈ ℕ
19. N : ℕ
20. (2 * n)^(k - 1) = N ∈ ℕ
21. r : {r:ℤ| |r| < |N|} 
22. ((x n)^k rem N) = r ∈ {r:ℤ| |r| < |N|} 
23. r1 : {r:ℤ| |r| < |M|} 
24. ((x m)^k rem M) = r1 ∈ {r:ℤ| |r| < |M|} 
⊢ |(M * m * (x n)^k) + ((-1) * M * m * r) + ((-1) * N * n * (x m)^k) + (N * n * r1)| ≤ ((2 * B * c * |M| * |N|)
  + (2 * c * |M| * |N|))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  k  :  \mBbbN{}\msupplus{}
3.  1  \mleq{}  2\^{}k  -  1
4.  v  :  \{3...\}
5.  canon-bnd(x)  =  v
6.  1  \mleq{}  2\^{}(k  -  1)
7.  n  :  \mBbbN{}\msupplus{}
8.  m  :  \mBbbN{}\msupplus{}
9.  \mforall{}n:\mBbbN{}\msupplus{}.  (|x  n|  \mleq{}  (n  *  v))
10.  0  \mleq{}  (v\^{}(k  -  1)  \mdiv{}  2\^{}(k  -  1))
11.  0  \mleq{}  (k  *  ((v\^{}(k  -  1)  \mdiv{}  2\^{}(k  -  1))  +  1))
\mvdash{}  |(m  *  ((x  n)\^{}k  \mdiv{}  (2  *  n)\^{}(k  -  1)))  -  n  *  ((x  m)\^{}k  \mdiv{}  (2  *  m)\^{}(k  -  1))|  \mleq{}  ((2
    *  ((k  *  ((v\^{}(k  -  1)  \mdiv{}  2\^{}(k  -  1))  +  1))  +  1))
    *  (n  +  m))


By

---

Latex:
(((GenConcl  \mkleeneopen{}(k  *  ((v\^{}(k  -  1)  \mdiv{}  2\^{}(k  -  1))  +  1))  =  B\mkleeneclose{}\mcdot{}  THENA  Auto)
    THEN  (GenConcl  \mkleeneopen{}(n  +  m)  =  c\mkleeneclose{}\mcdot{}  THENA  Auto)
    )
  THEN  (Assert  0  <  (2  *  n)\^{}(k  -  1)  \mwedge{}  0  <  (2  *  m)\^{}(k  -  1)  BY
                          Auto)
  THEN  (GenConcl  \mkleeneopen{}(2  *  m)\^{}(k  -  1)  =  M\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(2  *  n)\^{}(k  -  1)  =  N\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (MulAbs  \mkleeneopen{}N\mkleeneclose{}  0  \mcdot{}  THENA  Auto)
  THEN  (MulAbs  \mkleeneopen{}M\mkleeneclose{}  0  \mcdot{}  THENA  Auto)
  THEN  (RW  DivRemC  0  THENA  Auto)
  THEN  RepeatFor  2  ((GenRem  THENA  Auto))
  THEN  (RW  IntNormC  0  THENA  Auto))

---

Home Index