---

Step * 1 1 2 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
14. (a/b) - (1/n) < q * q
⊢ q * q < (a/b) + (1/n)
BY
{ ((QMul ⌜n⌝ (-3)⋅ THEN Auto) THEN QMul ⌜n⌝ 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. n * q * q < dv + 1
13. 0 ≤ q
14. (a/b) - (1/n) < q * q
⊢ n * q * q < 1 + ((a/b) * n)

---

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/n)  \mleq{}  (q  *  q)
12.  q  *  q  <  (dv  +  1/n)
13.  0  \mleq{}  q
14.  (a/b)  -  (1/n)  <  q  *  q
\mvdash{}  q  *  q  <  (a/b)  +  (1/n)


By

---

Latex:
((QMul  \mkleeneopen{}n\mkleeneclose{}  (-3)\mcdot{}  THEN  Auto)  THEN  QMul  \mkleeneopen{}n\mkleeneclose{}  0\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index