---

Step * 2 1 of Lemma square-between-lemma2

.....assertion..... 
1. n : ℕ+
2. k : ℕ
3. ¬k < n - 1
⊢ ∃b:ℕ+ [k < ((b * b) * n) - 1]
BY
{ TACTIC:((With ⌜isqrt(((k + 1) ÷ n) + 1) + 1⌝ (D 0)⋅ THEN Auto)⋅
          THEN (InstLemma `div_rem_sum` [⌜k + 1⌝;⌜n⌝]⋅ THENA Auto)
          THEN (InstLemma `rem_bounds_1` [⌜k + 1⌝;⌜n⌝]⋅ THENA Auto)
          THEN ((InstLemma `div_bounds_1` [⌜k + 1⌝;⌜n⌝]⋅ THEN Auto)
                THEN (InstLemma `isqrt-property` [((k + 1) ÷ n) + 1]⋅ THENA Auto)
                THEN MoveToConcl (-1)
                THEN GenConclAtAddr [1;1;1;1]
                THEN Thin (-1)
                THEN Auto)⋅) }

1
1. n : ℕ+
2. k : ℕ
3. ¬k < n - 1
4. (k + 1) = ((((k + 1) ÷ n) * n) + (k + 1 rem n)) ∈ ℤ
5. 0 ≤ (k + 1 rem n)
6. k + 1 rem n < n
7. 0 ≤ ((k + 1) ÷ n)
8. v : ℕ
9. (v * v) ≤ (((k + 1) ÷ n) + 1)
10. ((k + 1) ÷ n) + 1 < (v + 1) * (v + 1)
⊢ k < (((v + 1) * (v + 1)) * n) - 1

---

Latex:

---

Latex:
.....assertion..... 
1.  n  :  \mBbbN{}\msupplus{}
2.  k  :  \mBbbN{}
3.  \mneg{}k  <  n  -  1
\mvdash{}  \mexists{}b:\mBbbN{}\msupplus{}  [k  <  ((b  *  b)  *  n)  -  1]


By

---

Latex:
TACTIC:((With  \mkleeneopen{}isqrt(((k  +  1)  \mdiv{}  n)  +  1)  +  1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)\mcdot{}
                THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}k  +  1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}k  +  1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  ((InstLemma  `div\_bounds\_1`  [\mkleeneopen{}k  +  1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)
                            THEN  (InstLemma  `isqrt-property`  [((k  +  1)  \mdiv{}  n)  +  1]\mcdot{}  THENA  Auto)
                            THEN  MoveToConcl  (-1)
                            THEN  GenConclAtAddr  [1;1;1;1]
                            THEN  Thin  (-1)
                            THEN  Auto)\mcdot{})

---

Home Index