---

Step * 1 2 2 2 2 2 1 2 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. y : ℕ+
19. |a| * y^k < x^k * b^k
20. (x^k * b^k) ≤ ((|a| + d) * y^k)
21. (r(d)/r(b^k)) < (r1/r(n))
22. |a| = a ∈ ℤ
⊢ |(r(x)/r(y))^k - (r(a)/r(b^k))| < (r1/r(n))
BY
{ (HypSubst' (-1) (-4)
   THEN HypSubst' (-1) (-3)
   THEN Thin (-1)
   THEN ((Assert r0 < r(y)^k BY
                EAuto 1)
         THEN ((RWO "rnexp-rdiv<" 0 THENA Auto')
               THEN (RWO "rnexp-int" 0 THENA Auto')
               THEN (RepeatFor 3 (MoveToConcl (-2))
                     THEN (GenConcl ⌜x^k = X ∈ ℕ⌝⋅ THENA Auto')
                     THEN (GenConcl ⌜y^k = Z ∈ ℕ+⌝⋅ THENA Auto')
                     THEN ThinVar `y'
                     THEN ThinVar `x'
                     THEN GenConcl ⌜b^k = B ∈ ℕ+⌝⋅⋅
                     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))
⊢ |(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.  y  :  \mBbbN{}\msupplus{}
19.  |a|  *  y\^{}k  <  x\^{}k  *  b\^{}k
20.  (x\^{}k  *  b\^{}k)  \mleq{}  ((|a|  +  d)  *  y\^{}k)
21.  (r(d)/r(b\^{}k))  <  (r1/r(n))
22.  |a|  =  a
\mvdash{}  |(r(x)/r(y))\^{}k  -  (r(a)/r(b\^{}k))|  <  (r1/r(n))


By

---

Latex:
(HypSubst'  (-1)  (-4)
  THEN  HypSubst'  (-1)  (-3)
  THEN  Thin  (-1)
  THEN  ((Assert  r0  <  r(y)\^{}k  BY
                            EAuto  1)
              THEN  ((RWO  "rnexp-rdiv<"  0  THENA  Auto')
                          THEN  (RWO  "rnexp-int"  0  THENA  Auto')
                          THEN  (RepeatFor  3  (MoveToConcl  (-2))
                                      THEN  (GenConcl  \mkleeneopen{}x\^{}k  =  X\mkleeneclose{}\mcdot{}  THENA  Auto')
                                      THEN  (GenConcl  \mkleeneopen{}y\^{}k  =  Z\mkleeneclose{}\mcdot{}  THENA  Auto')
                                      THEN  ThinVar  `y'
                                      THEN  ThinVar  `x'
                                      THEN  GenConcl  \mkleeneopen{}b\^{}k  =  B\mkleeneclose{}\mcdot{}\mcdot{}
                                      THEN  Auto')\mcdot{})\mcdot{}
              )\mcdot{})\mcdot{}

---

Home Index