---

Step * of Lemma square-between-lemma1

∀n:ℕ+. ∀k:ℕn - 1.  (∃q:ℚ [(((k/n) ≤ (q * q)) ∧ q * q < (k + 1/n) ∧ (0 ≤ q))])
BY
{ (Auto
   THEN (With ⌜(isqrt((4 * n) * k) + 1/2 * n)⌝ (D 0)⋅ THENA Auto)
   THEN ((InstLemma `isqrt-property` [⌜(4 * n) * k⌝]⋅ THENA Auto) THEN MoveToConcl (-1))
   THEN (GenConclAtAddr [1;1;1;1] THENA Auto)
   THEN Thin (-1)
   THEN RenameVar `a' (-1)
   THEN Auto
   THEN RepeatFor 2 ((QMul ⌜2 * n⌝ 0⋅ THEN Auto THEN Try ((RWO "int-equal-in-rationals" 0 THEN Auto))))⋅
   THEN RepeatFor 2 ((RWW "qmul-mul" 0 THEN Auto))⋅) }

1
1. n : ℕ+
2. k : ℕn - 1
3. a : ℕ
4. (a * a) ≤ ((4 * n) * k)
5. (4 * n) * k < (a + 1) * (a + 1)
6. (k/n) ≤ ((a + 1/2 * n) * (a + 1/2 * n))
⊢ (a + 1) * (a + 1) < 4 * (k + 1) * n

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}k:\mBbbN{}n  -  1.    (\mexists{}q:\mBbbQ{}  [(((k/n)  \mleq{}  (q  *  q))  \mwedge{}  q  *  q  <  (k  +  1/n)  \mwedge{}  (0  \mleq{}  q))])


By

---

Latex:
(Auto
  THEN  (With  \mkleeneopen{}(isqrt((4  *  n)  *  k)  +  1/2  *  n)\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `isqrt-property`  [\mkleeneopen{}(4  *  n)  *  k\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  MoveToConcl  (-1))
  THEN  (GenConclAtAddr  [1;1;1;1]  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RenameVar  `a'  (-1)
  THEN  Auto
  THEN  RepeatFor  2  ((QMul  \mkleeneopen{}2  *  n\mkleeneclose{}  0\mcdot{}
                                        THEN  Auto
                                        THEN  Try  ((RWO  "int-equal-in-rationals"  0  THEN  Auto))))\mcdot{}
  THEN  RepeatFor  2  ((RWW  "qmul-mul"  0  THEN  Auto))\mcdot{})

---

Home Index