---

Step * of Lemma iroot-lemma2

∀a:ℕ. ∀n,b,k:ℕ+.  (∃p:ℕ × ℕ+ [let x,y = p in a * y^n < (x * b)^n ∧ ((x * b)^n ≤ ((a + k) * y^n))])
BY
{ (Auto
   THEN (With ⌜eval M = iroot(n;a + k) + 1 in
               eval y = ((n * b * M^n - 1) ÷ k) + 1 in
               eval x = iroot(n;(a + k) * y^n) ÷ b in
                 <x, y>⌝ (D 0)⋅
         THENA Try (Complete (Auto))
         )
   THEN (GenConcl ⌜(iroot(n;a + k) + 1) = M ∈ ℕ+⌝⋅ THENA Auto)
   THEN (CallByValueReduceOn ⌜M⌝ 0⋅ THENA Auto)
   THEN (Subst' M^n - 1 ~ M^(n - 1) 0 THEN Try ((Symmetry THEN BLemma `exp-fastexp` THEN Auto)))
   THEN (GenConcl ⌜(((n * b * M^(n - 1)) ÷ k) + 1) = y ∈ ℕ+⌝⋅
         THENA (Auto THEN InstLemma `div_bounds_1` [⌜n * b * M^(n - 1)⌝;⌜k⌝]⋅ THEN Auto)
         )
   THEN (CallByValueReduceOn ⌜y⌝ 0⋅ THENA Auto)
   THEN (Subst' y^n ~ y^n 0 THEN Try ((Symmetry THEN BLemma `exp-fastexp` THEN Auto)))
   THEN (GenConcl ⌜(iroot(n;(a + k) * y^n) ÷ b) = x ∈ ℕ⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Auto
   THEN Reduce 0) }

1
1. a : ℕ
2. n : ℕ+
3. b : ℕ+
4. k : ℕ+
5. M : ℕ+
6. (iroot(n;a + k) + 1) = M ∈ ℕ+
7. y : ℕ+
8. (((n * b * M^(n - 1)) ÷ k) + 1) = y ∈ ℕ+
9. x : ℕ
10. (iroot(n;(a + k) * y^n) ÷ b) = x ∈ ℕ
⊢ a * y^n < (x * b)^n ∧ ((x * b)^n ≤ ((a + k) * y^n))

---

Latex:

---

Latex:
\mforall{}a:\mBbbN{}.  \mforall{}n,b,k:\mBbbN{}\msupplus{}.    (\mexists{}p:\mBbbN{}  \mtimes{}  \mBbbN{}\msupplus{}  [let  x,y  =  p  in  a  *  y\^{}n  <  (x  *  b)\^{}n  \mwedge{}  ((x  *  b)\^{}n  \mleq{}  ((a  +  k)  *  y\^{}n))])


By

---

Latex:
(Auto
  THEN  (With  \mkleeneopen{}eval  M  =  iroot(n;a  +  k)  +  1  in
                          eval  y  =  ((n  *  b  *  M\^{}n  -  1)  \mdiv{}  k)  +  1  in
                          eval  x  =  iroot(n;(a  +  k)  *  y\^{}n)  \mdiv{}  b  in
                              <x,  y>\mkleeneclose{}  (D  0)\mcdot{}
              THENA  Try  (Complete  (Auto))
              )
  THEN  (GenConcl  \mkleeneopen{}(iroot(n;a  +  k)  +  1)  =  M\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}M\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Subst'  M\^{}n  -  1  \msim{}  M\^{}(n  -  1)  0  THEN  Try  ((Symmetry  THEN  BLemma  `exp-fastexp`  THEN  Auto)))
  THEN  (GenConcl  \mkleeneopen{}(((n  *  b  *  M\^{}(n  -  1))  \mdiv{}  k)  +  1)  =  y\mkleeneclose{}\mcdot{}
              THENA  (Auto  THEN  InstLemma  `div\_bounds\_1`  [\mkleeneopen{}n  *  b  *  M\^{}(n  -  1)\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THEN  Auto)
              )
  THEN  (CallByValueReduceOn  \mkleeneopen{}y\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Subst'  y\^{}n  \msim{}  y\^{}n  0  THEN  Try  ((Symmetry  THEN  BLemma  `exp-fastexp`  THEN  Auto)))
  THEN  (GenConcl  \mkleeneopen{}(iroot(n;(a  +  k)  *  y\^{}n)  \mdiv{}  b)  =  x\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Auto
  THEN  Reduce  0)

---

Home Index