---

Step * 2 1 of Lemma iroot-lemma

.....assertion..... 
1. a : ℕ
2. n : ℕ+
3. b : ℕ+
4. k : ℕ+
5. a + k ∈ ℕ+
6. M : ℕ+
7. a + k < M^n
⊢ ∃y:ℕ+. ((n * b * M^(n - 1)) ≤ (k * y))
BY
{ TACTIC:((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 With ⌜((n * b * M^(n - 1)) ÷ k) + 1⌝ (D 0)⋅
          THEN Auto
          THEN Auto') }

---

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
\mvdash{}  \mexists{}y:\mBbbN{}\msupplus{}.  ((n  *  b  *  M\^{}(n  -  1))  \mleq{}  (k  *  y))


By

---

Latex:
TACTIC:((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  With  \mkleeneopen{}((n  *  b  *  M\^{}(n  -  1))  \mdiv{}  k)  +  1\mkleeneclose{}  (D  0)\mcdot{}
                THEN  Auto
                THEN  Auto')

---

Home Index