---

Step * 1 1 1 of Lemma integer-between-reals


1. a : ℝ
2. b : ℝ
3. r(2) ≤ (b - a)
4. a < (a + r1)
5. (a + r1) < b
6. ∀k:ℤ. ((a < r(k)) ⇒ ((a < r(k - 1)) ∨ (r(k) < b)))
7. ∃u,v:ℤ. ((r(u) ≤ a) ∧ (a < r(v)))
8. d : ℤ
9. [%6] : 0 < d
10. ∀u:ℤ. ((r(u) ≤ a) ⇒ (a < r(u + (d - 1))) ⇒ (∃k:ℤ. ((a < r(k)) ∧ (r(k) < b))))
11. u : ℤ
12. r(u) ≤ a
13. a < r(u + d)
⊢ ∃k:ℤ. ((a < r(k)) ∧ (r(k) < b))
BY
{ ((FHyp 6 [-1] THEN Auto) THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  r(2)  \mleq{}  (b  -  a)
4.  a  <  (a  +  r1)
5.  (a  +  r1)  <  b
6.  \mforall{}k:\mBbbZ{}.  ((a  <  r(k))  {}\mRightarrow{}  ((a  <  r(k  -  1))  \mvee{}  (r(k)  <  b)))
7.  \mexists{}u,v:\mBbbZ{}.  ((r(u)  \mleq{}  a)  \mwedge{}  (a  <  r(v)))
8.  d  :  \mBbbZ{}
9.  [\%6]  :  0  <  d
10.  \mforall{}u:\mBbbZ{}.  ((r(u)  \mleq{}  a)  {}\mRightarrow{}  (a  <  r(u  +  (d  -  1)))  {}\mRightarrow{}  (\mexists{}k:\mBbbZ{}.  ((a  <  r(k))  \mwedge{}  (r(k)  <  b))))
11.  u  :  \mBbbZ{}
12.  r(u)  \mleq{}  a
13.  a  <  r(u  +  d)
\mvdash{}  \mexists{}k:\mBbbZ{}.  ((a  <  r(k))  \mwedge{}  (r(k)  <  b))


By

---

Latex:
((FHyp  6  [-1]  THEN  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index