---

Step * 2 2 2 1 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 ∈ ℕ+
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
⊢ (iroot(n;(a + k) * y^n) + 1)^n ≤ (((iroot(n;(a + k) * y^n) ÷ b) * b)^n + (n * b * (M * y)^(n - 1)))
BY
{ TACTIC:(InstLemma `mul_preserves_le` [⌜(iroot(n;(a + k) * y^n) + 1)^(n - 1)⌝;⌜(M * y)^(n - 1)⌝;⌜n * b⌝]⋅
          THENA (Auto THEN BLemma `exp_preserves_le` 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. 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
13. ((n * b) * (iroot(n;(a + k) * y^n) + 1)^(n - 1)) ≤ ((n * b) * (M * y)^(n - 1))
⊢ (iroot(n;(a + k) * y^n) + 1)^n ≤ (((iroot(n;(a + k) * y^n) ÷ b) * b)^n + (n * b * (M * y)^(n - 1)))

---

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{}
11.  iroot(n;(a  +  k)  *  y\^{}n)  <  M  *  y
12.  (iroot(n;(a  +  k)  *  y\^{}n)\^{}n  \mleq{}  ((a  +  k)  *  y\^{}n))  \mwedge{}  (a  +  k)  *  y\^{}n  <  (iroot(n;(a  +  k)  *  y\^{}n)  +  1)\^{}n
\mvdash{}  (iroot(n;(a  +  k)  *  y\^{}n)  +  1)\^{}n  \mleq{}  (((iroot(n;(a  +  k)  *  y\^{}n)  \mdiv{}  b)  *  b)\^{}n
    +  (n  *  b  *  (M  *  y)\^{}(n  -  1)))


By

---

Latex:
TACTIC:(InstLemma  `mul\_preserves\_le`  [\mkleeneopen{}(iroot(n;(a  +  k)  *  y\^{}n)  +  1)\^{}(n  -  1)\mkleeneclose{};\mkleeneopen{}(M  *  y)\^{}(n  -  1)\mkleeneclose{};\mkleeneopen{}n
                                                                                                                                                                                                *  b\mkleeneclose{}
                ]\mcdot{}
                THENA  (Auto  THEN  BLemma  `exp\_preserves\_le`  THEN  Auto)
                )

---

Home Index