---

Step * 1 1 1 2 of Lemma iroot-lemma2


1. n : ℕ+
2. a : ℕ
3. k : ℕ+
4. y : ℕ+
5. b : ℕ+
6. M : ℕ+
7. a + k ∈ ℕ+
8. a + k < M^n
9. (n * b * M^(n - 1)) ≤ (k * y)
10. (a + k) * y^n ∈ ℕ+
11. iroot(n;(a + k) * y^n) < M * y
⊢ a * y^n < ((iroot(n;(a + k) * y^n) ÷ b) * b)^n
BY
{ (InstLemma `iroot-property` [⌜n⌝;⌜(a + k) * y^n⌝]⋅ THENA Auto) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(InstLemma  `iroot-property`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}(a  +  k)  *  y\^{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index