---

Step * 1 1 1 1 1 1 1 1 1 of Lemma rroot-abs-property


1. i : {2...}
2. i ≠ 0
3. C : {2...}
4. n : ℕ+
5. b : ℕ
6. 2^(i - 1) = b ∈ ℕ
7. k : ℕ+
8. (n * n^(i - 1)) = k ∈ ℕ+
9. A : ℕ
10. B : ℕ
11. |(n * A) - k * B| ≤ (2 * (k + n))
12. R : ℕ
13. R^i ≤ (b * A)
14. b * A < (R + 1)^i
15. |R| ≤ ((2 * n) * C)
16. 0 < (2 * n)^(i - 1)
⊢ |k * ((R^i ÷ (2 * n)^(i - 1)) - B)| ≤ (k * ((i * b * C^(i - 1)) + 5))
BY
{ (MoveToConcl 11 THEN RevHypSubst' 8 0) }

1
1. i : {2...}
2. i ≠ 0
3. C : {2...}
4. n : ℕ+
5. b : ℕ
6. 2^(i - 1) = b ∈ ℕ
7. k : ℕ+
8. (n * n^(i - 1)) = k ∈ ℕ+
9. A : ℕ
10. B : ℕ
11. R : ℕ
12. R^i ≤ (b * A)
13. b * A < (R + 1)^i
14. |R| ≤ ((2 * n) * C)
15. 0 < (2 * n)^(i - 1)
⊢ (|(n * A) - (n * n^(i - 1)) * B| ≤ (2 * ((n * n^(i - 1)) + n)))
⇒ (|(n * n^(i - 1)) * ((R^i ÷ (2 * n)^(i - 1)) - B)| ≤ ((n * n^(i - 1)) * ((i * b * C^(i - 1)) + 5)))

---

Latex:

---

Latex:

1.  i  :  \{2...\}
2.  i  \mneq{}  0
3.  C  :  \{2...\}
4.  n  :  \mBbbN{}\msupplus{}
5.  b  :  \mBbbN{}
6.  2\^{}(i  -  1)  =  b
7.  k  :  \mBbbN{}\msupplus{}
8.  (n  *  n\^{}(i  -  1))  =  k
9.  A  :  \mBbbN{}
10.  B  :  \mBbbN{}
11.  |(n  *  A)  -  k  *  B|  \mleq{}  (2  *  (k  +  n))
12.  R  :  \mBbbN{}
13.  R\^{}i  \mleq{}  (b  *  A)
14.  b  *  A  <  (R  +  1)\^{}i
15.  |R|  \mleq{}  ((2  *  n)  *  C)
16.  0  <  (2  *  n)\^{}(i  -  1)
\mvdash{}  |k  *  ((R\^{}i  \mdiv{}  (2  *  n)\^{}(i  -  1))  -  B)|  \mleq{}  (k  *  ((i  *  b  *  C\^{}(i  -  1))  +  5))


By

---

Latex:
(MoveToConcl  11  THEN  RevHypSubst'  8  0)

---

Home Index