Step
*
2
1
1
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))
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|}
25. |(M * m * (x n)^k) + ((-1) * M * m * r) + ((-1) * N * n * (x m)^k) + (N * n * r1)| ≤ (|(M * m * (x n)^k) - N
* n
* (x m)^k|
+ |-(M * m * r)|
+ |N * n * r1|)
⊢ (|(M * m * (x n)^k) - N * n * (x m)^k| + |-(M * m * r)| + |N * n * r1|) ≤ ((2 * B * c * |M| * |N|)
+ (2 * c * |M| * |N|))
BY
{ ((Assert |N * n * r1| ≤ (n * |M| * |N|) BY
(DVar `r1'
THEN Unhide
THEN Auto
THEN (MulAbs ⌜N * n⌝ (-3)⋅ THENA Auto)
THEN (RW IntNormC (-1) THENA Auto)
THEN (RWO "-1" 0 THENA Auto)
THEN (RWW "absval_mul" 0 THENA Auto)
THEN Subst' |n| ~ n 0
THEN Auto))⋅
THEN (RWO "-1" 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|}
25. |(M * m * (x n)^k) + ((-1) * M * m * r) + ((-1) * N * n * (x m)^k) + (N * n * r1)| ≤ (|(M * m * (x n)^k) - N
* n
* (x m)^k|
+ |-(M * m * r)|
+ |N * n * r1|)
26. |N * n * r1| ≤ (n * |M| * |N|)
⊢ (|(M * m * (x n)^k) - N * n * (x m)^k| + |-(M * m * r)| + (n * |M| * |N|)) ≤ ((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))
12. B : \mBbbN{}
13. (k * ((v\^{}(k - 1) \mdiv{} 2\^{}(k - 1)) + 1)) = B
14. c : \mBbbN{}\msupplus{}
15. (n + m) = c
16. 0 < (2 * n)\^{}(k - 1) \mwedge{} 0 < (2 * m)\^{}(k - 1)
17. M : \mBbbN{}
18. (2 * m)\^{}(k - 1) = M
19. N : \mBbbN{}
20. (2 * n)\^{}(k - 1) = N
21. r : \{r:\mBbbZ{}| |r| < |N|\}
22. ((x n)\^{}k rem N) = r
23. r1 : \{r:\mBbbZ{}| |r| < |M|\}
24. ((x m)\^{}k rem M) = r1
25. |(M * m * (x n)\^{}k) + ((-1) * M * m * r) + ((-1) * N * n * (x m)\^{}k) + (N * n * r1)| \mleq{} (|(M
* m
* (x
n)\^{}k)
- N
* n
* (x m)\^{}k|
+ |-(M * m * r)|
+ |N * n * r1|)
\mvdash{} (|(M * m * (x n)\^{}k) - N * n * (x m)\^{}k| + |-(M * m * r)| + |N * n * r1|) \mleq{} ((2 * B * c * |M| * |N|)
+ (2 * c * |M| * |N|))
By
Latex:
((Assert |N * n * r1| \mleq{} (n * |M| * |N|) BY
(DVar `r1'
THEN Unhide
THEN Auto
THEN (MulAbs \mkleeneopen{}N * n\mkleeneclose{} (-3)\mcdot{} THENA Auto)
THEN (RW IntNormC (-1) THENA Auto)
THEN (RWO "-1" 0 THENA Auto)
THEN (RWW "absval\_mul" 0 THENA Auto)
THEN Subst' |n| \msim{} n 0
THEN Auto))\mcdot{}
THEN (RWO "-1" 0 THENA Auto)
)
Home
Index