---

Step * 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)))
⊢ ∃k:ℤ. ((a < r(k)) ∧ (r(k) < b))
BY
{ Assert ⌜∀d:ℕ. ∀u:ℤ.  ((r(u) ≤ a) ⇒ (a < r(u + d)) ⇒ (∃k:ℤ. ((a < r(k)) ∧ (r(k) < b))))⌝⋅ }

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

2
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:ℕ. ∀u:ℤ.  ((r(u) ≤ a) ⇒ (a < r(u + d)) ⇒ (∃k:ℤ. ((a < r(k)) ∧ (r(k) < b))))
⊢ ∃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.  \mexists{}u,v:\mBbbZ{}.  ((r(u)  \mleq{}  a)  \mwedge{}  (a  <  r(v)))
\mvdash{}  \mexists{}k:\mBbbZ{}.  ((a  <  r(k))  \mwedge{}  (r(k)  <  b))


By

---

Latex:
Assert  \mkleeneopen{}\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))))\mkleeneclose{}\mcdot{}

---

Home Index