---

Step * 2 2 1 2 2 of Lemma square-between-lemma2


1. n : ℕ+
2. k : ℕ
3. ¬k < n - 1
4. b : ℕ+
5. [%4] : k < ((b * b) * n) - 1
6. c : ℤ
7. c = b ∈ ℤ
8. k < ((c * c) * n) - 1
9. 0 < c
⊢ ∃q:ℚ [(((k/n) ≤ (q * q)) ∧ q * q < (k + 1/n) ∧ (0 ≤ q))]
BY
{ ((InstLemma `square-between-lemma1` [⌜(c * c) * n⌝;⌜k⌝] ⋅ THENA Auto)
   THEN D -1
   THEN With ⌜c * q⌝ (D 0)⋅
   THEN Auto
   THEN Try (Complete ((QMul ⌜c⌝ (-3)⋅ THEN Auto)))
   THEN QMul ⌜n⌝ 0⋅
   THEN Auto
   THEN QMul ⌜(c * c) * n⌝ (-3)⋅
   THEN Auto
   THEN RWO "qmul-mul" 0
   THEN Auto
   THEN RWO "int-equal-in-rationals" 0
   THEN Auto
   THEN (D 0 THENM D -1)
   THEN Auto
   THEN (FLemma `int_entire` [-1] THENM D -1)
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  k  :  \mBbbN{}
3.  \mneg{}k  <  n  -  1
4.  b  :  \mBbbN{}\msupplus{}
5.  [\%4]  :  k  <  ((b  *  b)  *  n)  -  1
6.  c  :  \mBbbZ{}
7.  c  =  b
8.  k  <  ((c  *  c)  *  n)  -  1
9.  0  <  c
\mvdash{}  \mexists{}q:\mBbbQ{}  [(((k/n)  \mleq{}  (q  *  q))  \mwedge{}  q  *  q  <  (k  +  1/n)  \mwedge{}  (0  \mleq{}  q))]


By

---

Latex:
((InstLemma  `square-between-lemma1`  [\mkleeneopen{}(c  *  c)  *  n\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]  \mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  With  \mkleeneopen{}c  *  q\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((QMul  \mkleeneopen{}c\mkleeneclose{}  (-3)\mcdot{}  THEN  Auto)))
  THEN  QMul  \mkleeneopen{}n\mkleeneclose{}  0\mcdot{}
  THEN  Auto
  THEN  QMul  \mkleeneopen{}(c  *  c)  *  n\mkleeneclose{}  (-3)\mcdot{}
  THEN  Auto
  THEN  RWO  "qmul-mul"  0
  THEN  Auto
  THEN  RWO  "int-equal-in-rationals"  0
  THEN  Auto
  THEN  (D  0  THENM  D  -1)
  THEN  Auto
  THEN  (FLemma  `int\_entire`  [-1]  THENM  D  -1)
  THEN  Auto)\mcdot{}

---

Home Index