---

Step * 1 1 1 1 of Lemma square-between-lemma3


1. a : ℕ
2. b : ℕ+
3. n : ℕ+
4. q : ℚ
5. rm : ℤ
6. dv : ℤ
7. (a * n) = ((dv * b) + rm) ∈ ℤ
8. 0 ≤ dv
9. 0 ≤ rm
10. rm < b
11. dv ≤ (n * q * q)
12. q * q < (dv + 1/n)
13. 0 ≤ q
⊢ (-1) + ((a/b) * n) < n * q * q
BY
{ (QMul ⌜b⌝ 0⋅ THEN Auto)⋅ }

1
1. a : ℕ
2. b : ℕ+
3. n : ℕ+
4. q : ℚ
5. rm : ℤ
6. dv : ℤ
7. (a * n) = ((dv * b) + rm) ∈ ℤ
8. 0 ≤ dv
9. 0 ≤ rm
10. rm < b
11. dv ≤ (n * q * q)
12. q * q < (dv + 1/n)
13. 0 ≤ q
⊢ -(b) + (a * n) < b * n * q * q

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}
2.  b  :  \mBbbN{}\msupplus{}
3.  n  :  \mBbbN{}\msupplus{}
4.  q  :  \mBbbQ{}
5.  rm  :  \mBbbZ{}
6.  dv  :  \mBbbZ{}
7.  (a  *  n)  =  ((dv  *  b)  +  rm)
8.  0  \mleq{}  dv
9.  0  \mleq{}  rm
10.  rm  <  b
11.  dv  \mleq{}  (n  *  q  *  q)
12.  q  *  q  <  (dv  +  1/n)
13.  0  \mleq{}  q
\mvdash{}  (-1)  +  ((a/b)  *  n)  <  n  *  q  *  q


By

---

Latex:
(QMul  \mkleeneopen{}b\mkleeneclose{}  0\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index