---

Step * 5 of Lemma i-member-proper-iff


1. y : Top
2. y1 : ℝ
3. iproper(<inr y , inl (inr y1 )>)
4. r : ℝ
5. b : {2...}
6. r(-b) < r
7. r < r(b)
8. m : ℕ+
9. r ≤ (y1 - (r1/r(m)))
⊢ ∃n:ℕ+. (iproper([r(-n), y1 - (r1/r(n))]) ∧ (r(-n) ≤ r) ∧ (r ≤ (y1 - (r1/r(n)))))
BY
{ (Assert ∃k:ℕ+. ((r(-k) ≤ r(-b)) ∧ ((y1 - (r1/r(m))) ≤ (y1 - (r1/r(k))))) BY
         (With ⌜imax(b;m)⌝ (D 0)⋅
          THEN Auto
          THEN Repeat ((RWO "imax_unfold" 0 THEN Auto))
          THEN AutoSplit
          THEN nRAdd ⌜-(y1)⌝ 0⋅
          THEN Auto
          THEN RWW "rminus-rdiv rminus-int" 0
          THEN Auto)) }

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

---

Latex:

---

Latex:

1.  y  :  Top
2.  y1  :  \mBbbR{}
3.  iproper(<inr  y  ,  inl  (inr  y1  )>)
4.  r  :  \mBbbR{}
5.  b  :  \{2...\}
6.  r(-b)  <  r
7.  r  <  r(b)
8.  m  :  \mBbbN{}\msupplus{}
9.  r  \mleq{}  (y1  -  (r1/r(m)))
\mvdash{}  \mexists{}n:\mBbbN{}\msupplus{}.  (iproper([r(-n),  y1  -  (r1/r(n))])  \mwedge{}  (r(-n)  \mleq{}  r)  \mwedge{}  (r  \mleq{}  (y1  -  (r1/r(n)))))


By

---

Latex:
(Assert  \mexists{}k:\mBbbN{}\msupplus{}.  ((r(-k)  \mleq{}  r(-b))  \mwedge{}  ((y1  -  (r1/r(m)))  \mleq{}  (y1  -  (r1/r(k)))))  BY
              (With  \mkleeneopen{}imax(b;m)\mkleeneclose{}  (D  0)\mcdot{}
                THEN  Auto
                THEN  Repeat  ((RWO  "imax\_unfold"  0  THEN  Auto))
                THEN  AutoSplit
                THEN  nRAdd  \mkleeneopen{}-(y1)\mkleeneclose{}  0\mcdot{}
                THEN  Auto
                THEN  RWW  "rminus-rdiv  rminus-int"  0
                THEN  Auto))

---

Home Index