---

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


1. k : {2...}
2. p : ℤ
3. q : ℕ+
4. n : ℕ+
5. (0 ≤ p) ∨ (↑isOdd(k))
6. s : 𝔹
7. s = (q =z 1) ∧b (n =z 1)
8. b : ℕ+
9. b = if s then 2 else q * n fi  ∈ ℕ+
10. c : ℕ+
11. c = b^(k - 1) ∈ ℕ+
12. a : ℤ
13. a = if s then p * 2 * c else p * n * c fi  ∈ ℤ
14. d : ℕ+
15. d = (if s then 2 * c else c fi  - 1) ∈ ℕ+
16. x : ℕ
17. y : ℕ+
18. |a| * y^k < x^k * b^k
19. (x^k * b^k) ≤ ((|a| + d) * y^k)
20. (r(d)/r(b^k)) < (r1/r(n))
21. p < 0
22. |a| = (-a) ∈ ℤ
⊢ |(r(-x)/r(y))^k - (r(a)/r(b^k))| < (r1/r(n))
BY
{ (HypSubst' (-1) (-5)
   THEN HypSubst' (-1) (-4)
   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 Try ((Subst ⌜-x ~ (-1) * x⌝ 0⋅
                          THEN Auto
                          THEN (RWO "exp-of-mul" 0 THENA Auto')
                          THEN (RWO "exp-minusone" 0 THENA Auto')
                          THEN AutoSplit
                          THEN Try ((D 5
                                     THEN Auto
                                     THEN Unfold `isOdd` 5
                                     THEN RW assert_pushdownC 5
                                     THEN Complete (Auto))))⋅)
               THEN (RepeatFor 3 (MoveToConcl (-3))
                     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. 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))

---

Latex:

---

Latex:

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


By

---

Latex:
(HypSubst'  (-1)  (-5)
  THEN  HypSubst'  (-1)  (-4)
  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  Try  ((Subst  \mkleeneopen{}-x  \msim{}  (-1)  *  x\mkleeneclose{}  0\mcdot{}
                                                THEN  Auto
                                                THEN  (RWO  "exp-of-mul"  0  THENA  Auto')
                                                THEN  (RWO  "exp-minusone"  0  THENA  Auto')
                                                THEN  AutoSplit
                                                THEN  Try  ((D  5
                                                                      THEN  Auto
                                                                      THEN  Unfold  `isOdd`  5
                                                                      THEN  RW  assert\_pushdownC  5
                                                                      THEN  Complete  (Auto))))\mcdot{})
                          THEN  (RepeatFor  3  (MoveToConcl  (-3))
                                      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