---

Step * 2 2 of Lemma square-between-lemma2


1. n : ℕ+
2. k : ℕ
3. ¬k < n - 1
4. ∃b:ℕ+ [k < ((b * b) * n) - 1]
⊢ ∃q:ℚ [(((k/n) ≤ (q * q)) ∧ q * q < (k + 1/n) ∧ (0 ≤ q))]
BY
{ (D (-1) THEN (Evaluate ⌜c = b ∈ ℤ⌝⋅ THENA Auto)) }

1
1. n : ℕ+
2. k : ℕ
3. ¬k < n - 1
4. b : ℕ+
5. [%4] : k < ((b * b) * n) - 1
6. c : ℤ
7. c = b ∈ ℤ
⊢ ∃q:ℚ [(((k/n) ≤ (q * q)) ∧ q * q < (k + 1/n) ∧ (0 ≤ q))]

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  k  :  \mBbbN{}
3.  \mneg{}k  <  n  -  1
4.  \mexists{}b:\mBbbN{}\msupplus{}  [k  <  ((b  *  b)  *  n)  -  1]
\mvdash{}  \mexists{}q:\mBbbQ{}  [(((k/n)  \mleq{}  (q  *  q))  \mwedge{}  q  *  q  <  (k  +  1/n)  \mwedge{}  (0  \mleq{}  q))]


By

---

Latex:
(D  (-1)  THEN  (Evaluate  \mkleeneopen{}c  =  b\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index