---

Step * 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^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)
BY
{ ((RWO "exp-fastexp<" 0 THENA Auto)
   THEN (Assert 0 < (2 * n)^(i - 1) BY
               (BLemma `exp-positive` THEN Auto))
   THEN (Assert ⌜|k| ~ k⌝⋅ THENA ((RWO  "absval_unfold" 0 THENA Auto) THEN AutoSplit))
   THEN Mul ⌜k⌝ 0⋅
   THEN RevHypSubst' (-1) 0
   THEN (RWO "absval_mul<" 0 THENA 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)
16. 0 < (2 * n)^(i - 1)
17. |k| ~ k
⊢ |k * ((R^i ÷ (2 * n)^(i - 1)) - B)| ≤ (|k| * ((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.  |(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)
\mvdash{}  |(R\^{}i  \mdiv{}  2  *  n\^{}i  -  1)  -  B|  \mleq{}  ((i  *  b  *  C\^{}(i  -  1))  +  5)


By

---

Latex:
((RWO  "exp-fastexp<"  0  THENA  Auto)
  THEN  (Assert  0  <  (2  *  n)\^{}(i  -  1)  BY
                          (BLemma  `exp-positive`  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}|k|  \msim{}  k\mkleeneclose{}\mcdot{}  THENA  ((RWO    "absval\_unfold"  0  THENA  Auto)  THEN  AutoSplit))
  THEN  Mul  \mkleeneopen{}k\mkleeneclose{}  0\mcdot{}
  THEN  RevHypSubst'  (-1)  0
  THEN  (RWO  "absval\_mul<"  0  THENA  Auto))

---

Home Index