---

Step * of Lemma integer-between-reals

No Annotations
∀a,b:ℝ.  ((r(2) ≤ (b - a)) ⇒ (∃k:ℤ. ((a < r(k)) ∧ (r(k) < b))))
BY
{ (Auto
   THEN (Assert a < (a + r1) BY
               Auto)
   THEN (Assert (a + r1) < b BY
               (nRAdd ⌜-(a)⌝ 0⋅ THEN Auto THEN nRNorm (-2) THEN RWO "-2<" 0 THEN Auto))
   THEN (Assert ∀k:ℤ. ((a < r(k)) ⇒ ((a < r(k - 1)) ∨ (r(k) < b))) BY
               (Auto
                THEN (InstLemma `rless-cases1` [⌜a⌝;⌜a + r1⌝;⌜r(k - 1)⌝]⋅ THENA Auto)
                THEN ParallelLast
                THEN nRAdd ⌜r1⌝ (-1)⋅
                THEN nRAdd ⌜a⌝ 3⋅
                THEN Auto))
   THEN (Assert ∃u,v:ℤ. ((r(u) ≤ a) ∧ (a < r(v))) BY
               ((InstLemma `canonical-bound-property` [⌜a⌝]⋅ THENA Auto)
                THEN InstConcl [⌜-canonical-bound(a)⌝;⌜canonical-bound(a) + 1⌝]⋅
                THEN Auto
                THEN RWO "-2" 0
                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)))
⊢ ∃k:ℤ. ((a < r(k)) ∧ (r(k) < b))

---

Latex:

---

Latex:
No  Annotations
\mforall{}a,b:\mBbbR{}.    ((r(2)  \mleq{}  (b  -  a))  {}\mRightarrow{}  (\mexists{}k:\mBbbZ{}.  ((a  <  r(k))  \mwedge{}  (r(k)  <  b))))


By

---

Latex:
(Auto
  THEN  (Assert  a  <  (a  +  r1)  BY
                          Auto)
  THEN  (Assert  (a  +  r1)  <  b  BY
                          (nRAdd  \mkleeneopen{}-(a)\mkleeneclose{}  0\mcdot{}  THEN  Auto  THEN  nRNorm  (-2)  THEN  RWO  "-2<"  0  THEN  Auto))
  THEN  (Assert  \mforall{}k:\mBbbZ{}.  ((a  <  r(k))  {}\mRightarrow{}  ((a  <  r(k  -  1))  \mvee{}  (r(k)  <  b)))  BY
                          (Auto
                            THEN  (InstLemma  `rless-cases1`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a  +  r1\mkleeneclose{};\mkleeneopen{}r(k  -  1)\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  ParallelLast
                            THEN  nRAdd  \mkleeneopen{}r1\mkleeneclose{}  (-1)\mcdot{}
                            THEN  nRAdd  \mkleeneopen{}a\mkleeneclose{}  3\mcdot{}
                            THEN  Auto))
  THEN  (Assert  \mexists{}u,v:\mBbbZ{}.  ((r(u)  \mleq{}  a)  \mwedge{}  (a  <  r(v)))  BY
                          ((InstLemma  `canonical-bound-property`  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  InstConcl  [\mkleeneopen{}-canonical-bound(a)\mkleeneclose{};\mkleeneopen{}canonical-bound(a)  +  1\mkleeneclose{}]\mcdot{}
                            THEN  Auto
                            THEN  RWO  "-2"  0
                            THEN  Auto)\mcdot{}))

---

Home Index