---

Step * 2 2 2 2 1 1 of Lemma iroot-lemma


1. a : ℕ
2. n : ℕ+
3. b : ℕ+
4. k : ℕ+
5. a + k ∈ ℕ+
6. M : ℕ+
7. a + k < M^n
8. y : ℕ+
9. (n * b * M^(n - 1)) ≤ (k * y)
10. (a + k) * y^n ∈ ℕ+
11. a * y^n < ((iroot(n;(a + k) * y^n) ÷ b) * b)^n
12. v : ℕ+
13. ((a + k) * y^n) = v ∈ ℕ+
14. iroot(n;v)^n ≤ v
15. v < (iroot(n;v) + 1)^n
⊢ ((iroot(n;v) ÷ b) * b)^n ≤ v
BY
{ (InstLemma `exp_preserves_le` [⌜n⌝;⌜(iroot(n;v) ÷ b) * b⌝;⌜iroot(n;v)⌝]⋅
   THEN Auto
   THEN (InstLemma `div_rem_sum` [⌜iroot(n;v)⌝;⌜b⌝]⋅ THENA Auto)
   THEN (InstLemma `rem_bounds_1` [⌜iroot(n;v)⌝;⌜b⌝]⋅ THENA Auto)
   THEN (InstLemma `div_bounds_1` [⌜iroot(n;v)⌝;⌜b⌝]⋅ THEN Auto)⋅)⋅ }

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}
2.  n  :  \mBbbN{}\msupplus{}
3.  b  :  \mBbbN{}\msupplus{}
4.  k  :  \mBbbN{}\msupplus{}
5.  a  +  k  \mmember{}  \mBbbN{}\msupplus{}
6.  M  :  \mBbbN{}\msupplus{}
7.  a  +  k  <  M\^{}n
8.  y  :  \mBbbN{}\msupplus{}
9.  (n  *  b  *  M\^{}(n  -  1))  \mleq{}  (k  *  y)
10.  (a  +  k)  *  y\^{}n  \mmember{}  \mBbbN{}\msupplus{}
11.  a  *  y\^{}n  <  ((iroot(n;(a  +  k)  *  y\^{}n)  \mdiv{}  b)  *  b)\^{}n
12.  v  :  \mBbbN{}\msupplus{}
13.  ((a  +  k)  *  y\^{}n)  =  v
14.  iroot(n;v)\^{}n  \mleq{}  v
15.  v  <  (iroot(n;v)  +  1)\^{}n
\mvdash{}  ((iroot(n;v)  \mdiv{}  b)  *  b)\^{}n  \mleq{}  v


By

---

Latex:
(InstLemma  `exp\_preserves\_le`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}(iroot(n;v)  \mdiv{}  b)  *  b\mkleeneclose{};\mkleeneopen{}iroot(n;v)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}iroot(n;v)\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}iroot(n;v)\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `div\_bounds\_1`  [\mkleeneopen{}iroot(n;v)\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{})\mcdot{}

---

Home Index