---

Step * 2 2 2 1 1 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. (M * y) ≤ iroot(n;(a + k) * y^n)
12. (M^n * y^n) ≤ ((a + k) * y^n)
⊢ iroot(n;(a + k) * y^n) < M * y
BY
{ (InstLemma `mul_preserves_lt` [⌜a + k⌝;⌜M^n⌝;⌜y^n⌝]⋅ 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.  (M  *  y)  \mleq{}  iroot(n;(a  +  k)  *  y\^{}n)
12.  (M\^{}n  *  y\^{}n)  \mleq{}  ((a  +  k)  *  y\^{}n)
\mvdash{}  iroot(n;(a  +  k)  *  y\^{}n)  <  M  *  y


By

---

Latex:
(InstLemma  `mul\_preserves\_lt`  [\mkleeneopen{}a  +  k\mkleeneclose{};\mkleeneopen{}M\^{}n\mkleeneclose{};\mkleeneopen{}y\^{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index