---

Step * 1 of Lemma square-between-lemma3


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)
BY
{ TACTIC:(MoveToConcl (-1)
          THEN (InstLemma `div_rem_sum` [⌜a * n⌝;⌜b⌝]⋅ THENA Auto)
          THEN (InstLemma `div_bounds_1` [⌜a * n⌝;⌜b⌝]⋅ THENA Auto)
          THEN (InstLemma `rem_bounds_1` [⌜a * n⌝;⌜b⌝]⋅ THENA Auto)
          THEN RepeatFor 3 (MoveToConcl (-1))
          THEN GenConclAtAddr [1;3;2]
          THEN Thin (-1)
          THEN RenameVar `rm' (-1)
          THEN GenConclAtAddr [1;3;1;1]
          THEN Thin (-1)
          THEN RenameVar `dv' (-1)) }

1
1. a : ℕ
2. b : ℕ+
3. n : ℕ+
4. q : ℚ
5. rm : ℤ
6. dv : ℤ
⊢ ((a * n) = ((dv * b) + rm) ∈ ℤ)
⇒ (0 ≤ dv)
⇒ ((0 ≤ rm) ∧ rm < b)
⇒ (((dv/n) ≤ (q * q)) ∧ q * q < (dv + 1/n) ∧ (0 ≤ q))
⇒ ((a/b) - (1/n) < q * q ∧ q * q < (a/b) + (1/n) ∧ (0 ≤ q))

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}
2.  b  :  \mBbbN{}\msupplus{}
3.  n  :  \mBbbN{}\msupplus{}
4.  q  :  \mBbbQ{}
5.  (((a  *  n)  \mdiv{}  b/n)  \mleq{}  (q  *  q))  \mwedge{}  q  *  q  <  (((a  *  n)  \mdiv{}  b)  +  1/n)  \mwedge{}  (0  \mleq{}  q)
\mvdash{}  (a/b)  -  (1/n)  <  q  *  q  \mwedge{}  q  *  q  <  (a/b)  +  (1/n)  \mwedge{}  (0  \mleq{}  q)


By

---

Latex:
TACTIC:(MoveToConcl  (-1)
                THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}a  *  n\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (InstLemma  `div\_bounds\_1`  [\mkleeneopen{}a  *  n\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}a  *  n\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  RepeatFor  3  (MoveToConcl  (-1))
                THEN  GenConclAtAddr  [1;3;2]
                THEN  Thin  (-1)
                THEN  RenameVar  `rm'  (-1)
                THEN  GenConclAtAddr  [1;3;1;1]
                THEN  Thin  (-1)
                THEN  RenameVar  `dv'  (-1))

---

Home Index