---

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

.....assertion..... 
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 ∈ ℕ+
⊢ iroot(n;(a + k) * y^n) < M * y
BY
{ TACTIC:(Decide (M * y) ≤ iroot(n;(a + k) * y^n)
          THEN Auto
          THEN (Assert (M * y)^n ≤ ((a + k) * y^n) BY
                      (InstLemma `iroot-property` [⌜n⌝;⌜(a + k) * y^n⌝]⋅
                       THEN Auto
                       THEN InstLemma `exp_preserves_le` [⌜n⌝;⌜M * y⌝;⌜iroot(n;(a + k) * y^n)⌝]⋅
                       THEN Auto))) }

1
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 * y)^n ≤ ((a + k) * y^n)
⊢ iroot(n;(a + k) * y^n) < M * y

---

Latex:

---

Latex:
.....assertion..... 
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{}
\mvdash{}  iroot(n;(a  +  k)  *  y\^{}n)  <  M  *  y


By

---

Latex:
TACTIC:(Decide  (M  *  y)  \mleq{}  iroot(n;(a  +  k)  *  y\^{}n)
                THEN  Auto
                THEN  (Assert  (M  *  y)\^{}n  \mleq{}  ((a  +  k)  *  y\^{}n)  BY
                                        (InstLemma  `iroot-property`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}(a  +  k)  *  y\^{}n\mkleeneclose{}]\mcdot{}
                                          THEN  Auto
                                          THEN  InstLemma  `exp\_preserves\_le`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}M  *  y\mkleeneclose{};\mkleeneopen{}iroot(n;(a  +  k)  *  y\^{}n)\mkleeneclose{}]\mcdot{}
                                          THEN  Auto)))

---

Home Index