---

Step * 1 1 of Lemma square-between-lemma3


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))
BY
{ TACTIC: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
⊢ (a/b) - (1/n) < q * q

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

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:Auto

---

Home Index