---

Step * of Lemma square-between-lemma3

∀a:ℕ. ∀b,n:ℕ+.  (∃q:ℚ [((a/b) - (1/n) < q * q ∧ q * q < (a/b) + (1/n) ∧ (0 ≤ q))])
BY
{ (Auto
   THEN (Evaluate ⌜na = ((a * n) ÷ b) ∈ ℕ⌝⋅ THENA Auto)
   THEN (InstLemma `square-between-lemma2` [⌜n⌝;⌜na⌝]⋅ THENA Auto)
   THEN ParallelLast
   THEN Try (Complete (Auto))
   THEN HypSubst' (-3) (-1)
   THEN RepeatFor 2 (Thin (-3))) }

1
1. a : ℕ
2. b : ℕ+
3. n : ℕ+
4. q : ℚ
5. (((a * n) ÷ b/n) ≤ (q * q)) ∧ q * q < (((a * n) ÷ b) + 1/n) ∧ (0 ≤ q)
⊢ (a/b) - (1/n) < q * q ∧ q * q < (a/b) + (1/n) ∧ (0 ≤ q)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Evaluate  \mkleeneopen{}na  =  ((a  *  n)  \mdiv{}  b)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `square-between-lemma2`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}na\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelLast
  THEN  Try  (Complete  (Auto))
  THEN  HypSubst'  (-3)  (-1)
  THEN  RepeatFor  2  (Thin  (-3)))

---

Home Index