---

Step * 1 1 of Lemma integer-between-reals

.....assertion..... 
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)))
⊢ ∀d:ℕ. ∀u:ℤ.  ((r(u) ≤ a) ⇒ (a < r(u + d)) ⇒ (∃k:ℤ. ((a < r(k)) ∧ (r(k) < b))))
BY
{ (InductionOnNat THEN 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,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))

---

Latex:

---

Latex:
.....assertion..... 
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)))
\mvdash{}  \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))))


By

---

Latex:
(InductionOnNat  THEN  Auto)

---

Home Index