---

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

1
.....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))

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


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}(dv  +  1)  \mleq{}  (1  +  ((a/b)  *  n))\mkleeneclose{}\mcdot{}

---

Home Index