---

Step * 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^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))
BY
{ (∀h:hyp. (RWO "exp-fastexp<" h THENA Auto)  THEN (RWO "exp_step" 8 THENA Auto) THEN HypSubst' -1 0 THEN Thin (-1)) }

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. |(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))

---

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)
16.  0  <  (2  *  n)\^{}(i  -  1)
17.  |k|  \msim{}  k
\mvdash{}  |k  *  ((R\^{}i  \mdiv{}  (2  *  n)\^{}(i  -  1))  -  B)|  \mleq{}  (|k|  *  ((i  *  b  *  C\^{}(i  -  1))  +  5))


By

---

Latex:
(\mforall{}h:hyp.  (RWO  "exp-fastexp<"  h  THENA  Auto) 
  THEN  (RWO  "exp\_step"  8  THENA  Auto)
  THEN  HypSubst'  -1  0
  THEN  Thin  (-1))

---

Home Index