---

Step * 1 1 1 1 1 1 1 of Lemma implies-isometry


1. r : {r:ℝ| r0 < r} 
2. m : ℕ+
3. z : ℝ
4. r0 < z
⊢ ∃a,b:ℝ
   ((∃n,m:ℕ+. (a = (r(n)/r(m))))
   ∧ (∃n,m:ℕ+. (b = (r(n)/r(m))))
   ∧ (z ∈ (a * r, b * r))
   ∧ (((b * r) - a * r) ≤ (r1/r(m))))
BY
{ Assert ⌜∀x,y:ℝ.
            ((r0 < x)
            ⇒ (r0 < y)
            ⇒ (∃a,b:ℝ. ((∃n,m:ℕ+. (a = (r(n)/r(m)))) ∧ (∃n,m:ℕ+. (b = (r(n)/r(m)))) ∧ (x ∈ (a, b)) ∧ ((b - a) ≤ y))))⌝
⋅ }

1
.....assertion..... 
1. r : {r:ℝ| r0 < r} 
2. m : ℕ+
3. z : ℝ
4. r0 < z
⊢ ∀x,y:ℝ.
    ((r0 < x)
    ⇒ (r0 < y)
    ⇒ (∃a,b:ℝ. ((∃n,m:ℕ+. (a = (r(n)/r(m)))) ∧ (∃n,m:ℕ+. (b = (r(n)/r(m)))) ∧ (x ∈ (a, b)) ∧ ((b - a) ≤ y))))

2
1. r : {r:ℝ| r0 < r} 
2. m : ℕ+
3. z : ℝ
4. r0 < z
5. ∀x,y:ℝ.
     ((r0 < x)
     ⇒ (r0 < y)
     ⇒ (∃a,b:ℝ. ((∃n,m:ℕ+. (a = (r(n)/r(m)))) ∧ (∃n,m:ℕ+. (b = (r(n)/r(m)))) ∧ (x ∈ (a, b)) ∧ ((b - a) ≤ y))))
⊢ ∃a,b:ℝ
   ((∃n,m:ℕ+. (a = (r(n)/r(m))))
   ∧ (∃n,m:ℕ+. (b = (r(n)/r(m))))
   ∧ (z ∈ (a * r, b * r))
   ∧ (((b * r) - a * r) ≤ (r1/r(m))))

---

Latex:

---

Latex:

1.  r  :  \{r:\mBbbR{}|  r0  <  r\} 
2.  m  :  \mBbbN{}\msupplus{}
3.  z  :  \mBbbR{}
4.  r0  <  z
\mvdash{}  \mexists{}a,b:\mBbbR{}
      ((\mexists{}n,m:\mBbbN{}\msupplus{}.  (a  =  (r(n)/r(m))))
      \mwedge{}  (\mexists{}n,m:\mBbbN{}\msupplus{}.  (b  =  (r(n)/r(m))))
      \mwedge{}  (z  \mmember{}  (a  *  r,  b  *  r))
      \mwedge{}  (((b  *  r)  -  a  *  r)  \mleq{}  (r1/r(m))))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}x,y:\mBbbR{}.
                    ((r0  <  x)
                    {}\mRightarrow{}  (r0  <  y)
                    {}\mRightarrow{}  (\mexists{}a,b:\mBbbR{}
                              ((\mexists{}n,m:\mBbbN{}\msupplus{}.  (a  =  (r(n)/r(m))))
                              \mwedge{}  (\mexists{}n,m:\mBbbN{}\msupplus{}.  (b  =  (r(n)/r(m))))
                              \mwedge{}  (x  \mmember{}  (a,  b))
                              \mwedge{}  ((b  -  a)  \mleq{}  y))))\mkleeneclose{}\mcdot{}

---

Home Index