---

Step * 1 2 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 : ℤ
8. v : ℤ
9. r(u) ≤ a
10. a < r(v)
11. ∀d:ℕ. ∀u:ℤ.  ((r(u) ≤ a) ⇒ (a < r(u + d)) ⇒ (∃k:ℤ. ((a < r(k)) ∧ (r(k) < b))))
12. u < v
⊢ ∃k:ℤ. ((a < r(k)) ∧ (r(k) < b))
BY
{ (InstHyp [⌜v - u⌝;⌜u⌝] (-2)⋅ 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.  u  :  \mBbbZ{}
8.  v  :  \mBbbZ{}
9.  r(u)  \mleq{}  a
10.  a  <  r(v)
11.  \mforall{}d:\mBbbN{}.  \mforall{}u:\mBbbZ{}.    ((r(u)  \mleq{}  a)  {}\mRightarrow{}  (a  <  r(u  +  d))  {}\mRightarrow{}  (\mexists{}k:\mBbbZ{}.  ((a  <  r(k))  \mwedge{}  (r(k)  <  b))))
12.  u  <  v
\mvdash{}  \mexists{}k:\mBbbZ{}.  ((a  <  r(k))  \mwedge{}  (r(k)  <  b))


By

---

Latex:
(InstHyp  [\mkleeneopen{}v  -  u\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)

---

Home Index