---

Step * 1 of Lemma iroot-lemma2


1. a : ℕ
2. n : ℕ+
3. b : ℕ+
4. k : ℕ+
5. M : ℕ+
6. (iroot(n;a + k) + 1) = M ∈ ℕ+
7. y : ℕ+
8. (((n * b * M^(n - 1)) ÷ k) + 1) = y ∈ ℕ+
9. x : ℕ
10. (iroot(n;(a + k) * y^n) ÷ b) = x ∈ ℕ
⊢ a * y^n < (x * b)^n ∧ ((x * b)^n ≤ ((a + k) * y^n))
BY
{ ((Assert a + k ∈ ℕ+ BY
          Auto')
   THEN (Assert a + k < M^n BY
               ((InstLemma  `iroot-property` [⌜n⌝;⌜a + k⌝]⋅ THENA Auto') THEN Decide 0 < iroot(n;a + k) THEN Auto')⋅)
   THEN (Assert (n * b * M^(n - 1)) ≤ (k * y) BY
               ((Assert n * b * M^(n - 1) ∈ ℕ BY
                       Auto)
                THEN (InstLemma `div_rem_sum` [⌜n * b * M^(n - 1)⌝;⌜k⌝]⋅ THENA Auto)
                THEN ((InstLemma `rem_bounds_1` [⌜n * b * M^(n - 1)⌝;⌜k⌝]⋅ THENA Auto)
                      THEN (InstLemma `div_bounds_1` [⌜n * b * M^(n - 1)⌝;⌜k⌝]⋅ THEN Auto)⋅
                      )
                THEN RevHypSubst' 8 0
                THEN Auto')⋅))⋅ }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  a  +  k  \mmember{}  \mBbbN{}\msupplus{}  BY
                Auto')
  THEN  (Assert  a  +  k  <  M\^{}n  BY
                          ((InstLemma    `iroot-property`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}a  +  k\mkleeneclose{}]\mcdot{}  THENA  Auto')
                            THEN  Decide  0  <  iroot(n;a  +  k)
                            THEN  Auto')\mcdot{})
  THEN  (Assert  (n  *  b  *  M\^{}(n  -  1))  \mleq{}  (k  *  y)  BY
                          ((Assert  n  *  b  *  M\^{}(n  -  1)  \mmember{}  \mBbbN{}  BY
                                          Auto)
                            THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}n  *  b  *  M\^{}(n  -  1)\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  ((InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}n  *  b  *  M\^{}(n  -  1)\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                        THEN  (InstLemma  `div\_bounds\_1`  [\mkleeneopen{}n  *  b  *  M\^{}(n  -  1)\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{}
                                        )
                            THEN  RevHypSubst'  8  0
                            THEN  Auto')\mcdot{}))\mcdot{}

---

Home Index