---

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

.....assertion..... 
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
⊢ (dv + 1) ≤ (1 + ((a/b) * n))
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. n * q * q < dv + 1
13. 0 ≤ q
14. (a/b) - (1/n) < q * q
⊢ ((dv + 1) * b) ≤ (b + (a * n))

---

Latex:

---

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


By

---

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

---

Home Index