---

Step * of Lemma iroot-lemma

∀a:ℕ. ∀n,b,k:ℕ+.  ∃x:ℕ. ∃y:ℕ+. (a * y^n < (x * b)^n ∧ ((x * b)^n ≤ ((a + k) * y^n)))
BY
{ (Auto THEN (Assert a + k ∈ ℕ+ BY Auto') THEN Assert ⌜∃M:ℕ+. a + k < M^n⌝⋅) }

1
.....assertion..... 
1. a : ℕ
2. n : ℕ+
3. b : ℕ+
4. k : ℕ+
5. a + k ∈ ℕ+
⊢ ∃M:ℕ+. a + k < M^n

2
1. a : ℕ
2. n : ℕ+
3. b : ℕ+
4. k : ℕ+
5. a + k ∈ ℕ+
6. ∃M:ℕ+. a + k < M^n
⊢ ∃x:ℕ. ∃y:ℕ+. (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{}x:\mBbbN{}.  \mexists{}y:\mBbbN{}\msupplus{}.  (a  *  y\^{}n  <  (x  *  b)\^{}n  \mwedge{}  ((x  *  b)\^{}n  \mleq{}  ((a  +  k)  *  y\^{}n)))


By

---

Latex:
(Auto  THEN  (Assert  a  +  k  \mmember{}  \mBbbN{}\msupplus{}  BY  Auto')  THEN  Assert  \mkleeneopen{}\mexists{}M:\mBbbN{}\msupplus{}.  a  +  k  <  M\^{}n\mkleeneclose{}\mcdot{})

---

Home Index