---

Step * 1 2 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))))
⊢ ∃k:ℤ. ((a < r(k)) ∧ (r(k) < b))
BY
{ ((Assert r(u) < r(v) BY Auto) THEN (RWO "rless-int" (-1) THENA Auto)) }

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

---

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))))
\mvdash{}  \mexists{}k:\mBbbZ{}.  ((a  <  r(k))  \mwedge{}  (r(k)  <  b))


By

---

Latex:
((Assert  r(u)  <  r(v)  BY  Auto)  THEN  (RWO  "rless-int"  (-1)  THENA  Auto))

---

Home Index