---

Step * of Lemma square-between-lemma2

∀n:ℕ+. ∀k:ℕ.  (∃q:ℚ [(((k/n) ≤ (q * q)) ∧ q * q < (k + 1/n) ∧ (0 ≤ q))])
BY
{ (Auto THEN (Decide k < n - 1 THENA Auto)) }

1
1. n : ℕ+
2. k : ℕ
3. k < n - 1
⊢ ∃q:ℚ [(((k/n) ≤ (q * q)) ∧ q * q < (k + 1/n) ∧ (0 ≤ q))]

2
1. n : ℕ+
2. k : ℕ
3. ¬k < n - 1
⊢ ∃q:ℚ [(((k/n) ≤ (q * q)) ∧ q * q < (k + 1/n) ∧ (0 ≤ q))]

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (Decide  k  <  n  -  1  THENA  Auto))

---

Home Index