---

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


1. k : {2...}
2. p : ℤ
3. ¬p < 0
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. X : ℕ
18. Z : ℕ+
19. B : ℕ+
20. b^k = B ∈ ℕ+
21. a * Z < X * B
22. (X * B) ≤ ((a + d) * Z)
23. (r(d)/r(B)) < (r1/r(n))
⊢ |(r(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. p : ℤ
3. ¬p < 0
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. X : ℕ
18. Z : ℕ+
19. B : ℕ+
20. b^k = B ∈ ℕ+
21. a * Z < X * B
22. (X * B) ≤ ((a + d) * Z)
23. (r(d)/r(B)) < (r1/r(n))
24. (r(a)/r(B)) < (r(X)/r(Z))
25. (r(X)/r(Z)) ≤ ((r(a)/r(B)) + (r(d)/r(B)))
⊢ |(r(X)/r(Z)) - (r(a)/r(B))| < (r1/r(n))

---

Latex:

---

Latex:

1.  k  :  \{2...\}
2.  p  :  \mBbbZ{}
3.  \mneg{}p  <  0
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.  X  :  \mBbbN{}
18.  Z  :  \mBbbN{}\msupplus{}
19.  B  :  \mBbbN{}\msupplus{}
20.  b\^{}k  =  B
21.  a  *  Z  <  X  *  B
22.  (X  *  B)  \mleq{}  ((a  +  d)  *  Z)
23.  (r(d)/r(B))  <  (r1/r(n))
\mvdash{}  |(r(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)

---

Home Index