---

Step * 1 2 2 2 2 2 1 1 1 of Lemma near-root-rational


1. k : {2...}
2. k mod 2 ≠ 0
3. p : ℤ
4. q : ℕ+
5. n : ℕ+
6. (0 ≤ p) ∨ (↑isOdd(k))
7. s : 𝔹
8. s = (q =z 1) ∧b (n =z 1)
9. b : ℕ+
10. b = if s then 2 else q * n fi  ∈ ℕ+
11. c : ℕ+
12. c = b^(k - 1) ∈ ℕ+
13. a : ℤ
14. a = if s then p * 2 * c else p * n * c fi  ∈ ℤ
15. d : ℕ+
16. d = (if s then 2 * c else c fi  - 1) ∈ ℕ+
17. p < 0
18. X : ℕ
19. Z : ℕ+
20. B : ℕ+
21. b^k = B ∈ ℕ+
22. (-a) * Z < X * B
23. (X * B) ≤ (((-a) + d) * Z)
24. (r(d)/r(B)) < (r1/r(n))
⊢ |(r((-1) * X)/r(Z)) - (r(a)/r(B))| < (r1/r(n))
BY
{ (Assert ⌜((r(-a)/r(B)) < (r(X)/r(Z))) ∧ ((r(X)/r(Z)) ≤ ((r(-a)/r(B)) + (r(d)/r(B))))⌝⋅
   THEN Auto
   THEN RWW "radd-rdiv radd-int" 0
   THEN Auto)⋅ }

1
1. k : {2...}
2. k mod 2 ≠ 0
3. p : ℤ
4. q : ℕ+
5. n : ℕ+
6. (0 ≤ p) ∨ (↑isOdd(k))
7. s : 𝔹
8. s = (q =z 1) ∧b (n =z 1)
9. b : ℕ+
10. b = if s then 2 else q * n fi  ∈ ℕ+
11. c : ℕ+
12. c = b^(k - 1) ∈ ℕ+
13. a : ℤ
14. a = if s then p * 2 * c else p * n * c fi  ∈ ℤ
15. d : ℕ+
16. d = (if s then 2 * c else c fi  - 1) ∈ ℕ+
17. p < 0
18. X : ℕ
19. Z : ℕ+
20. B : ℕ+
21. b^k = B ∈ ℕ+
22. (-a) * Z < X * B
23. (X * B) ≤ (((-a) + d) * Z)
24. (r(d)/r(B)) < (r1/r(n))
25. (r(-a)/r(B)) < (r(X)/r(Z))
26. (r(X)/r(Z)) ≤ ((r(-a)/r(B)) + (r(d)/r(B)))
⊢ |(r((-1) * X)/r(Z)) - (r(a)/r(B))| < (r1/r(n))

---

Latex:

---

Latex:

1.  k  :  \{2...\}
2.  k  mod  2  \mneq{}  0
3.  p  :  \mBbbZ{}
4.  q  :  \mBbbN{}\msupplus{}
5.  n  :  \mBbbN{}\msupplus{}
6.  (0  \mleq{}  p)  \mvee{}  (\muparrow{}isOdd(k))
7.  s  :  \mBbbB{}
8.  s  =  (q  =\msubz{}  1)  \mwedge{}\msubb{}  (n  =\msubz{}  1)
9.  b  :  \mBbbN{}\msupplus{}
10.  b  =  if  s  then  2  else  q  *  n  fi 
11.  c  :  \mBbbN{}\msupplus{}
12.  c  =  b\^{}(k  -  1)
13.  a  :  \mBbbZ{}
14.  a  =  if  s  then  p  *  2  *  c  else  p  *  n  *  c  fi 
15.  d  :  \mBbbN{}\msupplus{}
16.  d  =  (if  s  then  2  *  c  else  c  fi    -  1)
17.  p  <  0
18.  X  :  \mBbbN{}
19.  Z  :  \mBbbN{}\msupplus{}
20.  B  :  \mBbbN{}\msupplus{}
21.  b\^{}k  =  B
22.  (-a)  *  Z  <  X  *  B
23.  (X  *  B)  \mleq{}  (((-a)  +  d)  *  Z)
24.  (r(d)/r(B))  <  (r1/r(n))
\mvdash{}  |(r((-1)  *  X)/r(Z))  -  (r(a)/r(B))|  <  (r1/r(n))


By

---

Latex:
(Assert  \mkleeneopen{}((r(-a)/r(B))  <  (r(X)/r(Z)))  \mwedge{}  ((r(X)/r(Z))  \mleq{}  ((r(-a)/r(B))  +  (r(d)/r(B))))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  RWW  "radd-rdiv  radd-int"  0
  THEN  Auto)\mcdot{}

---

Home Index