---

Step * 2 1 of Lemma i-member-proper-iff


1. u : ℝ
2. v : ℝ
3. r : ℝ
4. b : {2...}
5. r(-b) < r
6. r < r(b)
7. m : ℕ+
8. u ≤ (r - (r1/r(m)))
9. r ≤ v
10. u < v
⊢ ∃n:ℕ+. (iproper([u + (r1/r(n)), v]) ∧ ((u + (r1/r(n))) ≤ r) ∧ (r ≤ v))
BY
{ (Assert ∃k:ℕ+. (u < (v - (r1/r(k)))) BY
         ((InstLemma `small-reciprocal-real` [⌜v - u⌝]⋅ THENA (MemTypeCD THEN Auto THEN nRAdd ⌜u⌝ 0⋅ THEN Auto))
          THEN ParallelLast
          THEN Auto
          THEN (nRAdd ⌜u - (r1/r(k))⌝ (-1)⋅ THENA Auto)
          THEN nRNorm 0
          THEN Auto)) }

1
1. u : ℝ
2. v : ℝ
3. r : ℝ
4. b : {2...}
5. r(-b) < r
6. r < r(b)
7. m : ℕ+
8. u ≤ (r - (r1/r(m)))
9. r ≤ v
10. u < v
11. ∃k:ℕ+. (u < (v - (r1/r(k))))
⊢ ∃n:ℕ+. (iproper([u + (r1/r(n)), v]) ∧ ((u + (r1/r(n))) ≤ r) ∧ (r ≤ v))

---

Latex:

---

Latex:

1.  u  :  \mBbbR{}
2.  v  :  \mBbbR{}
3.  r  :  \mBbbR{}
4.  b  :  \{2...\}
5.  r(-b)  <  r
6.  r  <  r(b)
7.  m  :  \mBbbN{}\msupplus{}
8.  u  \mleq{}  (r  -  (r1/r(m)))
9.  r  \mleq{}  v
10.  u  <  v
\mvdash{}  \mexists{}n:\mBbbN{}\msupplus{}.  (iproper([u  +  (r1/r(n)),  v])  \mwedge{}  ((u  +  (r1/r(n)))  \mleq{}  r)  \mwedge{}  (r  \mleq{}  v))


By

---

Latex:
(Assert  \mexists{}k:\mBbbN{}\msupplus{}.  (u  <  (v  -  (r1/r(k))))  BY
              ((InstLemma  `small-reciprocal-real`  [\mkleeneopen{}v  -  u\mkleeneclose{}]\mcdot{}
                  THENA  (MemTypeCD  THEN  Auto  THEN  nRAdd  \mkleeneopen{}u\mkleeneclose{}  0\mcdot{}  THEN  Auto)
                  )
                THEN  ParallelLast
                THEN  Auto
                THEN  (nRAdd  \mkleeneopen{}u  -  (r1/r(k))\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
                THEN  nRNorm  0
                THEN  Auto))

---

Home Index