---

Step * 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^i = k ∈ ℕ+
9. A : ℕ
10. B : ℕ
11. |iroot(i;b * A)| ≤ ((2 * n) * C)
12. |(n * A) - k * B| ≤ (2 * (k + n))
⊢ |(iroot(i;b * A)^i ÷ 2 * n^i - 1) - B| ≤ ((i * b * C^(i - 1)) + 5)
BY
{ (MoveToConcl (-2)
   THEN (InstLemma `iroot-property` [⌜i⌝;⌜b * A⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜iroot(i;b * A) = R ∈ ℕ⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN Auto) }

1
1. i : {2...}
2. i ≠ 0
3. C : {2...}
4. n : ℕ+
5. b : ℕ
6. 2^(i - 1) = b ∈ ℕ
7. k : ℕ+
8. n^i = 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)
⊢ |(R^i ÷ 2 * n^i - 1) - B| ≤ ((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\^{}i  =  k
9.  A  :  \mBbbN{}
10.  B  :  \mBbbN{}
11.  |iroot(i;b  *  A)|  \mleq{}  ((2  *  n)  *  C)
12.  |(n  *  A)  -  k  *  B|  \mleq{}  (2  *  (k  +  n))
\mvdash{}  |(iroot(i;b  *  A)\^{}i  \mdiv{}  2  *  n\^{}i  -  1)  -  B|  \mleq{}  ((i  *  b  *  C\^{}(i  -  1))  +  5)


By

---

Latex:
(MoveToConcl  (-2)
  THEN  (InstLemma  `iroot-property`  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}b  *  A\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}iroot(i;b  *  A)  =  R\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Auto)

---

Home Index